proposition: Lemma pure_typing_tidyLR {s n} : is_simple s -> allfv_poly_type (gt n) s -> pure_typing [tidy (many_poly_abs n s)] (pure_var 0) (many_poly_abs n s).
proof: Proof. move=> Hs Hns. apply: (pure_typing_pure_var n); first by reflexivity. rewrite -tidy_ren_poly_type ren_poly_type_many_poly_abs. have -> : ren_poly_type (Nat.iter n up_ren (Nat.add n)) s = s. { rewrite -[RHS]ren_poly_type_id. apply: ext_ren_poly_type_allfv_poly_type. apply: allfv_poly_type_impl Hns. move=> ? ?. rewrite iter_up_ren_lt; by [|lia]. } rewrite -[s in contains _ s](tidy_is_simple Hs). apply: contains_tidyI. rewrite -[s in contains _ s]subst_poly_type_poly_var. by apply: contains_many_poly_abs_closedI. 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