proposition: Lemma deq_prod : forall (A B : Type), Deq A -> Deq B -> Deq (A * B).
proof: Proof. unfold Deq; introv da db; introv; sp. generalize (da x0 y0) (db x y); introv ea eb; sp; subst; sp; right; intro k; inversion k; sp. Defined.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega