proposition: Lemma stepK_expansion M N Gamma t : stepK M N -> type_assignment Gamma N t -> match M with | var _ => exists Gamma', type_assignment Gamma' M t | app _ _ => exists Gamma', type_assignment Gamma' M t | lam _ => typable M end.
proof: Proof. have Hty : forall M t, match M with | var _ => exists Gamma', type_assignment Gamma' M t | app _ _ => exists Gamma', type_assignment Gamma' M t | lam _ => typable M end -> typable M. { by move=> [] > => [[? /typable_intro]|[? /typable_intro]|]. } move=> H. elim: H Gamma t. - move=> > /nf_typable /arg_K_typable H. move=> Gamma t /(type_assignment_ren _ ((atom 0, nil):: Gamma) S) H'. apply: H. constructor. apply: H'. by case. - move=> > ? IH Gamma [] > /type_assignmentE; [done|]. move=> /IH /Hty. by apply: typable_lam. - move=> > ?? IH Gamma t /type_assignmentE [] >. move=> ? /IH /Hty {}IH ?. apply: neutral_typableE. constructor; [|done]. apply: neutral_typableI; [|econstructor]; eassumption. - move=> > ? IH Gamma t /type_assignmentE [] >. move=> ? /IH /Hty {}IH ?. by apply: arg_K_typable; eassumption. - move=> > ? IH Gamma t /type_assignmentE [] >. move=> /IH [?] ?? H. eexists (merge Gamma _). econstructor. + apply: type_assignment_mergeL. by eassumption. + by apply: type_assignment_mergeR. + apply: Forall_impl H => *. by apply: type_assignment_mergeR. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect