proposition: Lemma tidy_many_poly_abs {n s} : { n'ξ' | tidy (many_poly_abs n s) = many_poly_abs (n'ξ'.1) (tidy (ren_poly_type (n'ξ'.2) s)) }.
proof: Proof. elim: n s. - move=> s. exists (0, id). by rewrite ren_poly_type_id. - move=> n IH s /=. case Hns: (fresh_inb 0 (many_poly_abs n s)). + have := IH s. move=> [[n' ξ']] ->. rewrite ren_poly_type_many_poly_abs -tidy_ren_poly_type ?poly_type_norm. evar (n'': nat). evar (ξ'': nat -> nat). exists (n'', ξ'') => /=. by subst n'' ξ''. + have := IH s. move=> [[n' ξ']] ->. by exists ((1+n'), ξ'). 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