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