proposition: Lemma typing_ren_allfv_term {ξ Gamma Gamma' P t} : (allfv_term (fun x => nth_error Gamma x = nth_error Gamma' (ξ x)) P) -> typing Gamma P t -> typing Gamma' (ren_term id ξ P) t.
proof: Proof. elim: P ξ Gamma Gamma' t. - move=> > /= + /typingE => -> ?. by apply: typing_var. - move=> ? IH1 ? IH2 > /= [/IH1 {}IH1 /IH2 {}IH2]. move=> /typingE [?] [/IH1 ? /IH2 ?] /=. apply: typing_app; by eassumption. - move=> > IH > /= H /typingE [?] [->] /IH /= {}IH. rewrite ren_poly_type_id. apply: typing_abs. apply: IH. apply: allfv_term_impl H. by case. - move=> > IH > /IH {}IH. move=> /typingE [?] [->] /IH {}IH /=. rewrite ren_poly_type_id. by apply: typing_ty_app. - move=> > IH > /= H. move=> /typingE [?] [->] /IH {}IH /=. apply: typing_ty_abs. under extRen_term. + move=> ?. rewrite upRen_poly_type_poly_type_id. over. + move=> ?. rewrite /upRen_poly_type_term. over. + apply: IH. apply: allfv_term_impl H => ?. rewrite ?nth_error_map. by move=> ->. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts term_facts) ssreflect ssrbool ssrfun