proposition: Lemma nf_typable M : normal_form M -> typable M.
proof: Proof. elim. - move=> x. apply: (typable_intro _ (repeat ((atom 0), nil) (S x)) (atom 0)). econstructor; [|by left]. apply: nth_error_repeat. lia. - move=> > ?. by apply: typable_lam. - move=> x N ??. have /neutral_typableE : neutral typable (app (var x) N) by do ? constructor. move=> /(_ (atom 0)) [?] ?. econstructor. by eassumption. - move=> > /normal_form_app_neutral /neutral_typableI /[apply]. move=> /neutral_typableE H _ [] Gamma t ?. move: (H (arr t nil (atom 0))) => [Gamma'] ?. apply: typable_intro. econstructor. + apply: (type_assignment_mergeL Gamma Gamma'). by eassumption. + by apply: type_assignment_mergeR. + done. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect