proposition: Theorem eq_dec_refl {A : Type} `{EqDec_eq A} (x : A) : eq_dec x x = left eq_refl.
proof: Proof. destruct (eq_dec x x); [|contradiction]. f_equal; apply (Eqdep_dec.UIP_dec eq_dec). Qed.
imports: Coq.Classes.Equivalence Coq.Classes.EquivDec Coq.Logic.Decidable