proposition: Lemma DeqDeqp : forall {A : Type}, Deq A -> DeqP A.
proof: Proof. introv deq. intros x y. destruct (deq x y);[left|right]; auto. Qed.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega Coq.Logic.Eqdep_dec