proposition: Lemma tidy_ren_poly_type {ξ t} : tidy (ren_poly_type ξ t) = ren_poly_type ξ (tidy t).
proof: Proof. elim: t ξ; [done | by move=> ? + ? + ? /= => -> -> |]. move=> ? IH ξ /=. set b1 := (fresh_inb _ (ren_poly_type _ _)). move Hb2: (fresh_inb _ _) => b2. have ->: b1 = b2. { subst b2. apply /(sameP fresh_inP) /(equivP fresh_inP). rewrite /= allfv_poly_type_ren_poly_type. apply: ext_allfv_poly_type. by case. } case: b2 Hb2; last by rewrite /= IH. rewrite IH ?poly_type_norm => /fresh_inP H. apply: ext_ren_poly_type_allfv_poly_type. rewrite allfv_poly_type_tidy. apply: allfv_poly_type_impl H. by case. 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