proposition: Lemma equiv_symmetric' : forall (A : Type) `{EqDec A} (x y : A), x === y -> y === x.
proof: Proof. intros. apply equiv_symmetric; assumption. Qed.
imports: Coq.Classes.Equivalence Coq.Classes.EquivDec Coq.Logic.Decidable