proposition: Theorem in_fold_map: forall (A: Set) (f: nat -> nat -> A) p l1 l2, In p (fold_right (fun x l => map (f x) l1 ++ l) nil l2) <-> (exists x, (exists y , In x l2 /\ In y l1 /\ p = f x y)).
proof: Proof. intros A f p l1 l2; elim l2; simpl; auto; clear l2. split; auto. intros H; case H. intros (x, (y, (H, _))); auto. intros a l2 (Rec1, Rec2); split; intros H. case in_app_or with (1 := H); clear H; intros H. case (in_map_inv _ _ (f a) p l1); auto. intros y (H1, H2). exists a; exists y; repeat split; auto. case Rec1; auto; clear Rec1 Rec2. intros x (y, (U1, (U2, U3))); exists x; exists y; repeat split; auto with arith. case H; intros x (y, ([U1 | U1], (U2, U3))); subst; auto; clear H. apply in_or_app; left; auto. apply in_map; auto. apply in_or_app; right; auto. apply Rec2; auto; clear Rec1 Rec2. exists x; exists y; repeat split; auto with arith. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat