proposition: Lemma typing_subst_poly_type {Gamma P t} σ : typing Gamma P t -> typing (map (subst_poly_type σ) Gamma) (subst_term σ var P) (subst_poly_type σ t).
proof: Proof. elim: P Gamma t σ. - move=> > /typingE ? /=. apply: typing_var. by apply: map_nth_error. - move=> ? IH1 ? IH2 > /typingE [? [? ?]] /=. apply: typing_app; last by apply: IH2; eassumption. rewrite -/(subst_poly_type _ (poly_arr _ _)). by apply: IH1. - move=> s P IH > /typingE [?] [-> ?] /=. apply: typing_abs. rewrite -/(map _ (_ :: _)). rewrite ?term_norm. by apply: IH. - move=> P IH s Gamma t σ /typingE [t'] [-> /IH] /=. move=> /(_ σ) /typing_ty_app => /(_ (subst_poly_type σ s)). congr typing. rewrite ?poly_type_norm. apply: ext_poly_type => [[|x]]; first done. by rewrite /= ?poly_type_norm /= subst_poly_type_poly_var. - move=> P IH Gamma t σ /typingE [?] [-> /IH {}IH] /=. apply: typing_ty_abs. have := IH (poly_var 0 .: σ >> ren_poly_type S). congr typing. rewrite ?map_map. apply: map_ext. move=> ?. by rewrite ?poly_type_norm. 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