proposition: Lemma aux_pure_typing_gxs {Gamma x M n s} : nth_error Gamma x = Some (poly_abs (poly_var 0)) -> pure_typing Gamma M (Nat.iter n (fun s' : poly_type => poly_abs (poly_arr (poly_var 0) s')) s) -> pure_typing Gamma (many_pure_app M (repeat (pure_var x) n)) (many_poly_abs n s).
proof: Proof. move=> Hx HM. apply: pure_typing_many_poly_absI. elim: n s HM; first by (move=> >; rewrite map_ren_poly_type_id). move=> n IH s. rewrite (ltac:(lia) : S n = n + 1) repeat_app many_pure_app_app /= => HM. apply: (pure_typing_pure_app_simpleI (s := poly_var 0)). - have ->: map (ren_poly_type (Nat.add (n + 1))) Gamma = map (ren_poly_type S) (map (ren_poly_type (Nat.add n)) Gamma). { rewrite ?map_map. apply: map_ext => ?. rewrite poly_type_norm /=. by apply: extRen_poly_type; lia. } apply: (pure_typing_many_poly_absE (n := 1)). apply: IH. move: HM. by rewrite -iter_plus. - apply: (pure_typing_pure_var 0); first by rewrite ?nth_error_map Hx /=. by apply /rt_step /contains_step_subst. 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