Typeclass and notation for logical equivalence.

class Cslib.Logic.LogicalEquivalence {α : Type u_1} {Judgement : Type u_2} (S : Type u_3) (eqv : α → α → Prop) [HasContext α] [Congruence eqv] [HasHContext Judgement α] [InferenceSystem S Judgement] extends Cslib.LawfulCongruence eqv : Sort (max (max (u_1 + 1) (u_5 + 1)) u_6)

A logical equivalence eqv for an inference system S is a congruence on propositions (of type α) that preserves validity of judgements under any judgemental context.

• refl (a : α) : eqv a a
• trans (a b c : α) : eqv a b → eqv b c → eqv a c
• symm (a b : α) : eqv a b → eqv b a
• elim : Covariant (Cslib.HasContext.Context α) α (fun (x1 : Cslib.HasContext.Context α) (x2 : α) => x1<[x2]) fun (x1 x2 : α) => Cslib.Congruence.r eqv x1 x2
• eqvFillValid {a b : α} (heqv : Congruence.r eqv a b) (c : HasHContext.Context Judgement α) (h : InferenceSystem.derivation S c<[a]) : InferenceSystem.derivation S c<[b]

  Validity is preserved for any judgemental context.