proposition: Lemma stepI_expansion M N Gamma t : stepI M N -> type_assignment Gamma N t -> type_assignment Gamma M t.
proof: Proof. move=> H. elim: H Gamma t. - move=> *. by apply: stepISubst_expansion. - move=> > _ IH ? [|??] > /type_assignmentE ?; [done|]. constructor. by apply: IH. - move=> > _ IH > /type_assignmentE [] *. econstructor; [|eassumption..]. apply: IH. by eassumption. - move=> > _ IH > /type_assignmentE [] > ?? H'. econstructor. + by eassumption. + by apply: IH. + apply: Forall_impl H' => ?. by apply: IH. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect