proposition: Theorem Forall_Exists_exists_Forall2 l1 l2 : Forall (fun a => Exists (R a) l2) l1 -> exists l2', Forall2 l1 l2' /\ incl l2' l2.
proof: Proof. induction l1 as [|a l1 IH]. - intros _. now exists []. - intros [[b [Hb Hab]] %Exists_exists Hl1l2] %Forall_cons_iff. destruct (IH Hl1l2) as [l2' [Hl1l2' Hl2'l2]]. exists (b :: l2'). now eauto using incl_cons. Qed.
imports: PeanoNat