proposition: Lemma decidable_prod : forall (P Q: [univ]), decidable P -> decidable Q -> decidable (P * Q).
proof: Proof. introv Hpd Hqd. unfold decidable; destruct Hpd; destruct Hqd; try (left; dands; auto; fail); (right; introv Hc; repnd; auto). Defined.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega