proposition: Lemma ren_poly_type_poly_var_bound {ξ n t} : poly_var_bound t <= n -> ren_poly_type (Nat.iter n up_ren ξ) t = t.
proof: Proof. move=> H. apply: ren_poly_type_allfv_id. apply: allfv_poly_type_impl (poly_var_boundP t) => ? ?. apply: iter_up_ren_lt. by lia. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun