proposition: Lemma eq_reflexive_unfolded : forall x : S, x [=] x.
proof: Proof. Proof eq_reflexive. Lemma eq_symmetric_unfolded : forall x y : S, x [=] y -> y [=] x. Proof eq_symmetric. Lemma eq_transitive_unfolded : forall x y z : S, x [=] y -> y [=] z -> x [=] z. Proof eq_transitive. Lemma eq_wdl : forall x y z : S, x [=] y -> x [=] z -> z [=] y. Proof. intros. now apply (eq_transitive _ x);[apply: eq_symmetric|]. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid