proposition: Lemma type_assignment_ren_fv Gamma Delta xi t M : type_assignment Gamma M t -> allfv (fun x => forall s phi, nth_error Gamma x = Some (s, phi) -> nth_error Delta (xi x) = Some (s, phi)) M -> type_assignment Delta (ren xi M) t.
proof: Proof. elim: M Gamma Delta xi t. - move=> > /type_assignmentE [>] /= ++ IH. move=> /IH ??. by econstructor; eassumption. - move=> > IH1 > IH2 > /type_assignmentE [>]. move=> /IH1 {}IH1 ? Hphi /= [] /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. apply: allfv_impl H'. by case. Qed.
imports: Undecidability.IntersectionTypes.CD PeanoNat List Relations Lia Undecidability.LambdaCalculus.Lambda Undecidability.LambdaCalculus.Util.term_facts ssreflect