proposition: Lemma tidy_many_poly_abs_le {n t}: allfv_poly_type (le n) t -> tidy (many_poly_abs n t) = ren_poly_type (fun x => x - n) (tidy t).
proof: Proof. elim: n t. - move=> t _ /=. rewrite ren_poly_type_id'; by [|lia]. - move=> n IH t /= Ht. have ->: fresh_inb 0 (many_poly_abs n t) = true. { apply /fresh_inP. rewrite /fresh_in allfv_poly_type_many_poly_abs. apply: allfv_poly_type_impl Ht. move=> x ?. rewrite iter_scons_ge; by lia. } rewrite IH. { apply: allfv_poly_type_impl Ht. by lia. } rewrite poly_type_norm. apply: extRen_poly_type. move=> x /=. case H: (x-n) => /=; 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) ssreflect ssrbool ssrfun