proposition: Lemma pure_typable_tidy_iff {Gamma1 Gamma2 M} : Forall (fun t => exists n s, t = many_poly_abs n s /\ is_simple s /\ allfv_poly_type (gt n) s) Gamma2 -> pure_typable (Gamma1 ++ map tidy Gamma2) M <-> pure_typable (Gamma1 ++ Gamma2) M.
proof: Proof. elim: Gamma2 Gamma1; first done. move=> ? Gamma2 IH Gamma1 /Forall_cons_iff [] [n] [s] [->] [Hs Hns] /IH {}IH. constructor => /=. - move=> [?] /pure_typing_weaken_closed => /(_ (many_poly_abs n s)). apply: unnest. { rewrite allfv_poly_type_many_poly_abs. apply: allfv_poly_type_impl Hns. move=> *. rewrite iter_scons_lt; by [|lia]. } apply: unnest; first by apply: pure_typing_tidyRL. rewrite -/([_] ++ map tidy Gamma2) -/([_] ++ Gamma2) ?app_assoc. by move=> /pure_typableI /IH. - move=> [?] /pure_typing_weaken_closed => /(_ (tidy (many_poly_abs n s))). apply: unnest. { rewrite allfv_poly_type_tidy allfv_poly_type_many_poly_abs. apply: allfv_poly_type_impl Hns. move=> *. rewrite iter_scons_lt; by [|lia]. } apply: unnest; first by apply: pure_typing_tidyLR. rewrite -/([_] ++ map tidy Gamma2) -/([_] ++ Gamma2) ?app_assoc. by move=> /pure_typableI /IH. 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