proposition: Lemma DeqTrue: forall {A} (deq : Deq A) (a : A), (deq a a) = (left (@eq_refl A a)).
proof: Proof. intros; auto. destruct (deq a a) as [HH| HH]. - f_equal. apply UIPReflDeq; auto. - destruct HH. auto. Defined.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega Coq.Logic.Eqdep_dec