proposition: Lemma arg_K_typable M N Gamma s phi t : type_assignment Gamma (lam (ren S M)) (arr s phi t) -> typable N -> exists Gamma', type_assignment Gamma' (app (lam (ren S M)) N) t.
proof: Proof. move=> /type_assignmentE ? [] Gamma' s' ?. exists (merge Gamma Gamma'). econstructor; [|by apply: type_assignment_mergeL; eassumption|by apply: Forall_nil]. apply: type_assignment_mergeR. constructor. apply: type_assignment_fv; [eassumption|]. apply: allfv_ren. apply: allfv_trivial. move=> >. by apply. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect