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