proposition: Lemma typing_many_ty_appI {Gamma P n t ts} : length ts = n -> typing Gamma P (many_poly_abs n t) -> typing Gamma (many_ty_app P ts) (subst_poly_type (fold_right scons poly_var (rev ts)) t).
proof: Proof. elim: n Gamma P t ts. - move=> ? ? ? [|]; last done. move=> _ /=. congr typing. by rewrite subst_poly_type_poly_var. - move=> n IH Gamma P t. elim /rev_ind; first done. move=> s ts'. rewrite app_length /many_poly_abs -iter_last -/(many_poly_abs _ _) /=. move=> ? ?. have /IH {}IH : length ts' = n by lia. move=> /IH {}IH. rewrite rev_unit many_ty_app_app /=. move: IH => /= => /typing_ty_app => /(_ s). congr typing. rewrite ?poly_type_norm. apply: ext_poly_type => [[|x]]; first done. by rewrite /= ?poly_type_norm /= subst_poly_type_poly_var. 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