proposition: Lemma typing_subst_term {Gamma Delta P t} σ : typing Gamma P t -> (forall n s, nth_error Gamma n = Some s -> typing Delta (σ n) s) -> typing Delta (subst_term poly_var σ P) t.
proof: Proof. move=> H. elim: H σ Delta. - by move=> > + > H => /H. - move=> > ? IH1 ? IH2 > H /=. apply: typing_app; [by apply: IH1 | by apply: IH2]. - move=> > ? IH > H /=. rewrite subst_poly_type_poly_var ?term_norm. apply: typing_abs. apply: IH => [[|n]] ?. + move=> /= [<-]. by apply: typing_var. + move=> /H /typing_ren_term. apply. by case. - move=> > _ IH > ? /=. rewrite subst_poly_type_poly_var. by apply /typing_ty_app /IH. - move=> {}Gamma > _ IH > H /=. under ext_term => [? | ?] do [rewrite up_poly_type_poly_type_poly_var |]. apply /typing_ty_abs /IH => n' s'. rewrite nth_error_map. case Hn': (nth_error Gamma n'); last done. move: Hn' => /H {}H [<-]. by apply: typing_ren_poly_type. 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