proposition: Theorem in_list_prod_inv: forall (A B : Set) a l1 l2, In a (list_prod l1 l2) -> (exists b : A , exists c : B , a = (b, c) /\ (In b l1 /\ In c l2) ).
proof: Proof. intros A B a l1 l2; elim l1; simpl; auto; clear l1. intros H; case H. intros a1 l1 H1 H2. case in_app_or with ( 1 := H2 ); intros H3; auto. case in_map_inv with ( 1 := H3 ); intros b1 [Hb1 Hb2]; auto. exists a1; exists b1; split; auto. case H1; auto; intros b1 [c1 [Hb1 [Hb2 Hb3]]]. exists b1; exists c1; split; auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat