proposition: Lemma neutral_typableE M : neutral typable M -> forall t, exists Gamma, type_assignment Gamma M t.
proof: Proof. elim. - move=> x t. exists (repeat (t, nil) (S x)). econstructor. + apply: nth_error_repeat. lia. + by left. - move=> > _ IH [] Gamma s ? t. move: (IH (arr s nil t)) => - [Gamma'] ?. exists (merge Gamma Gamma'). econstructor. + apply: type_assignment_mergeL. 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