proposition: Lemma subst_poly_type_map_seq {f n t} : poly_var_bound t <= n -> subst_poly_type (fold_right scons poly_var (map f (seq 0 n))) t = subst_poly_type f t.
proof: Proof. move=> H. apply: ext_subst_poly_type_allfv_poly_type. apply: allfv_poly_type_impl (poly_var_boundP t) => x ?. apply: fold_right_map_seq. by lia. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun