proposition: Lemma pure_typing_many_poly_absE {n Gamma M t} : pure_typing Gamma M (many_poly_abs n t) -> pure_typing (map (ren_poly_type (Nat.add n)) Gamma) M t.
proof: Proof. elim: n Gamma t. - move=> > /=. by rewrite map_ren_poly_type_id. - move=> n IH Gamma t /=. move=> /(pure_typing_ren_poly_type S) /pure_typing_to_typing [?] [?] /=. move=> /typing_ty_app => /(_ (poly_var 0)). subst M. rewrite ?poly_type_norm subst_poly_type_poly_var'; first by case. move=> /typing_to_pure_typing /= /IH. congr pure_typing. rewrite ?map_map. apply: map_ext => ?. rewrite ?poly_type_norm /=. apply: extRen_poly_type. by lia. Qed.
imports: List Lia Relation_Definitions Relation_Operators Operators_Properties Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts iipc2_facts) ssreflect ssrbool ssrfun