Tealeaves.Util.EqDec_eq
Require Export Coq.Classes.EquivDec.
Require Export Coq.Structures.Equalities.
Set Implicit Arguments.
Class EqDec_eq (A : Type) :=
eq_dec : forall (x y : A), {x = y} + {x <> y}.
Instance EqDec_eq_of_EqDec (A : Type) `(@EqDec A eq eq_equivalence) : EqDec_eq A.
Proof. trivial. Defined.
Declare Scope coqeqdec_scope.
Notation "x == y" := (eq_dec x y) (at level 70) : coqeqdec_scope.
Open Scope coqeqdec_scope.
Theorem eq_dec_refl {A : Type} `{EqDec_eq A} (x : A) : eq_dec x x = left eq_refl.
Proof.
destruct (eq_dec x x); [|contradiction].
f_equal; apply (Eqdep_dec.UIP_dec eq_dec).
Qed.
Require Export Coq.Structures.Equalities.
Set Implicit Arguments.
Class EqDec_eq (A : Type) :=
eq_dec : forall (x y : A), {x = y} + {x <> y}.
Instance EqDec_eq_of_EqDec (A : Type) `(@EqDec A eq eq_equivalence) : EqDec_eq A.
Proof. trivial. Defined.
Declare Scope coqeqdec_scope.
Notation "x == y" := (eq_dec x y) (at level 70) : coqeqdec_scope.
Open Scope coqeqdec_scope.
Theorem eq_dec_refl {A : Type} `{EqDec_eq A} (x : A) : eq_dec x x = left eq_refl.
Proof.
destruct (eq_dec x x); [|contradiction].
f_equal; apply (Eqdep_dec.UIP_dec eq_dec).
Qed.