proposition: Lemma allfv_poly_type_tidy {P t} : allfv_poly_type P (tidy t) <-> allfv_poly_type P t.
proof: Proof. elim: t P; [done | by move=> /= ? + ? + ? => -> -> |]. move=> ? IH ? /=. case H: (fresh_inb _ _); last by apply: IH. rewrite allfv_poly_type_ren_poly_type IH. apply: ext_allfv_poly_type_allfv_poly_type. move: H => /(fresh_inP). apply: allfv_poly_type_impl. 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