proposition: Theorem mProd_correct : forall (A B C : Set) (l1 : list A) (l2 : list B) (a : A) (b : B), In a l1 -> In b l2 -> In (a, b) (mProd A B C l1 l2).
proof: Proof. intros A B C l1 l2; elim l2; simpl in |- *; auto. intros a l H' a0 b H'0 H'1; elim H'1; [ intros H'2; rewrite <- H'2; clear H'1 | intros H'2; clear H'1 ]; auto with datatypes. apply in_or_app; left; auto with datatypes. generalize H'0; elim l1; simpl in |- *; auto with datatypes. intros a1 l0 H'1 H'3; elim H'3; clear H'3; intros H'4; [ rewrite <- H'4 | idtac ]; auto with datatypes. Qed.
imports: Reals ZArith List PeanoNat Psatz