proposition: Lemma eq_class_expand x y z (D: r x z \/ r z x \/ r y z \/ r z y) : eqv x ≡₁ eqv y <-> eqv x y.
proof: Proof. Proof using REFL SYM TRAN. u; intuition; eauto. Qed.
imports: HahnBase HahnSets HahnRelationsBasic Setoid HahnEquational