proposition: Lemma tidy_subst_poly_type {σ t} : tidy (subst_poly_type σ t) = subst_poly_type (σ >> tidy) (tidy t).
proof: Proof. elim: t σ; [done | by move=> ? + ? + ? /= => -> -> |]. move=> ? IH σ /=. set b1 := (fresh_inb _ (subst_poly_type _ _)). move Hb2: (fresh_inb _ _) => b2. have ->: b1 = b2. { subst b2. apply /(sameP fresh_inP) /(equivP fresh_inP). rewrite /= allfv_poly_type_subst_poly_type. apply: ext_allfv_poly_type. case; first done. move=> ?. rewrite /= allfv_poly_type_ren_poly_type /=. constructor; last done. move=> _. by apply: allfv_poly_type_TrueI. } case: b2 Hb2. - rewrite IH ?poly_type_norm => /fresh_inP H. apply: ext_subst_poly_type_allfv_poly_type. rewrite allfv_poly_type_tidy. apply: allfv_poly_type_impl H. case; first done. move=> ? _ /=. by rewrite tidy_ren_poly_type ?poly_type_norm ren_poly_type_id. - move=> _ /=. rewrite IH /=. congr poly_abs. apply: ext_poly_type. case; first done. move=> ?. by rewrite /= tidy_ren_poly_type. 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