class Cslib.Congruence (α : Type u_1) [HasContext α] (r : α → α → Prop) extends IsEquiv α r, CovariantClass (Cslib.HasContext.Context α) α (fun (x1 : Cslib.HasContext.Context α) (x2 : α) => x1<[x2]) r : Prop

An equivalence relation on α preserved by all contexts Ctx.

• refl (a : α) : r a a
• trans (a b c : α) : r a b → r b c → r a c
• symm (a b : α) : r a b → r b a
• elim : Covariant (Cslib.HasContext.Context α) α (fun (x1 : Cslib.HasContext.Context α) (x2 : α) => x1<[x2]) r