proposition: Lemma typing_many_ty_absI {n Gamma P t}: typing (map (ren_poly_type (Nat.add n)) Gamma) P t -> typing Gamma (many_ty_abs n P) (many_poly_abs n t).
proof: Proof. elim: n Gamma P t. - move=> >. under map_ext => ? do rewrite /= ren_poly_type_id. by rewrite map_id. - move=> n IH > H /=. apply: typing_ty_abs. apply: IH. move: H. congr typing. rewrite map_map. apply: map_ext. move=> ?. rewrite ?poly_type_norm. apply: extRen_poly_type. move=> ?. rewrite /funcomp /=. by lia. 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