proposition: Lemma type_assignment_subst Gamma Delta sigma t M : type_assignment Gamma M t -> (forall x s phi, nth_error Gamma x = Some (s, phi) -> Forall (type_assignment Delta (sigma x)) (s::phi)) -> type_assignment Delta (subst sigma M) t.
proof: Proof. elim: M Gamma Delta sigma t. - move=> > /type_assignmentE [>] /= ++ IH. move=> /IH /Forall_cons_iff [IH1 /Forall_forall IH2]. by move=> [<-|/IH2]. - move=> > IH1 > IH2 > /type_assignmentE [>]. move=> /IH1 {}IH1 ? Hphi /[dup] /IH1 ? /IH2 {}IH2 /=. econstructor. + eassumption. + by apply: IH2. + by apply: Forall_impl Hphi => ? /IH2. - move=> > IH ??? [] > /type_assignmentE; first done. move=> /IH {}IH H' /=. constructor. apply: IH. move=> [|x] > /=. + move=> [<- <-]. apply /Forall_forall=> ??. by econstructor. + move=> /H'. apply: Forall_impl=> ? /type_assignment_ren. by apply. Qed.
imports: Undecidability.IntersectionTypes.CD PeanoNat List Relations Lia Undecidability.LambdaCalculus.Lambda Undecidability.LambdaCalculus.Util.term_facts ssreflect