proposition: Lemma typable_lam M : typable M -> typable (lam M).
proof: Proof. move=> [] [|[??] ?] ?. + move=> /(type_assignment_mergeL [(atom 0, nil)]) ?. do 2 econstructor. by eassumption. + move=> *. do 2 econstructor. by eassumption. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect