proposition: Lemma contains_tidyI {t t'} : contains t t' -> contains (tidy t) (tidy t').
proof: Proof. move=> /clos_rt_rt1n_iff. elim; first by move=> ?; apply: rt_refl. move=> > [] s'' t'' _ IH /=. case H: (fresh_inb _ _). - move: IH. rewrite tidy_subst_poly_type. congr contains. rewrite ren_as_subst_poly_type. apply: ext_subst_poly_type_allfv_poly_type. rewrite allfv_poly_type_tidy. move: H => /fresh_inP. apply: allfv_poly_type_impl. by case. - apply: rt_trans; last by eassumption. apply: rt_step. rewrite tidy_subst_poly_type. have := contains_step_subst (s := tidy s'') (t := tidy t''). congr contains_step. apply: ext_poly_type. 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