proposition: Lemma Forall_exists_Forall2 {X Y : Type} (P : X -> Y -> Prop) l : Forall (fun x => exists (y : Y), P x y) l -> exists l', Forall2 P l l'.
proof: Proof. elim. - by exists nil. - move=> ?? [y ?] _ [l' ?]. exists (y :: l'). by constructor. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect