proposition: Lemma Forall_In_impl {X : Type} {P Q : X -> Prop} {l : list X} : (forall x, In x l -> P x -> Q x) -> Forall P l -> Forall Q l.
proof: Proof. move=> ? /Forall_forall ?. apply /Forall_forall. by auto with nocore. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun