proposition: Lemma neutral_typableI P M : neutral P M -> typable M -> neutral typable M.
proof: Proof. elim. - by constructor. - move=> > _ IH _ [] > /type_assignmentE [] *. constructor; [apply: IH|]; apply: typable_intro; eassumption. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect