proposition: Fact list_exists X Y (R : X -> Y -> Prop) l : (forall x, In x l -> exists y, R x y) -> exists ll, Forall2 R l ll.
proof: Proof. induction l as [ | x l IHl ]; intros Hl. exists nil; constructor. destruct (Hl x) as (y & Hy). left; auto. destruct IHl as (ll & Hll). intros; apply Hl; right; auto. exists (y::ll); constructor; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)