proposition: Lemma type_preservation_step {Gamma t M N} : step M N -> type_assignment Gamma M t -> type_assignment Gamma N t.
proof: Proof. move=> H. elim: H Gamma t. - move=> > /type_assignmentE [>] /type_assignmentE *. apply: type_assignment_subst; [eassumption|]. move=> [|x]. + move=> ?? [<- <-]. by constructor. + move=> ?? /= Hx. apply /Forall_forall=> ? Ht. by econstructor; eassumption. - move=> > ? IH > /type_assignmentE []. by eauto using type_assignment with nocore. - move=> > ? IH > /type_assignmentE []. eauto using type_assignment, Forall_impl with nocore. - move=> > ? IH ? [] > /type_assignmentE; by eauto using type_assignment with nocore. Qed.
imports: Undecidability.IntersectionTypes.CD PeanoNat List Relations Lia Undecidability.LambdaCalculus.Lambda Undecidability.LambdaCalculus.Util.term_facts ssreflect