proposition: Lemma UIPReflDeq: forall { A : Type} (deq : Deq A) (a: A) (p: a=a), p= eq_refl.
proof: Proof. intros. remember (@eq_refl A a) as eqr. apply UIP_dec. auto. Qed.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega Coq.Logic.Eqdep_dec