proposition: Lemma equiv_decidable : forall (A : Type) `{EqDec A} (x y : A), decidable (x === y).
proof: Proof. intros. unfold decidable. destruct (x == y); auto. Defined.
imports: Coq.Classes.Equivalence Coq.Classes.EquivDec Coq.Logic.Decidable