proposition: Lemma aux_pure_typable_gys {Gamma x M n s} : nth_error Gamma x = Some (poly_var 0) -> pure_typing Gamma M (Nat.iter n (fun s' : poly_type => poly_abs (poly_arr (poly_var 0) s')) s) -> pure_typable Gamma (many_pure_app M (repeat (pure_var x) n)).
proof: Proof. move=> Hx HM. exists (ren_poly_type (fun x => x - n) s). elim: n s HM. { move=> > /=. rewrite ren_poly_type_id'; by [|lia]. } move=> n IH s. rewrite (ltac:(lia) : S n = n + 1) repeat_app many_pure_app_app /=. rewrite -iter_plus /= => /IH /pure_typing_to_typing [?] [->] /=. move=> /(typing_ty_app (t := poly_var 0)) /= /(typing_app (Q := var x)). apply: unnest; first by apply: typing_var. move=> /typing_to_pure_typing /=. congr pure_typing. rewrite poly_type_norm ren_as_subst_poly_type /=. apply: ext_poly_type. case; first done. move=> ?. congr poly_var. 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 pure_typing_facts) ssreflect ssrbool ssrfun