∀ {S : Type u_4} [inst : CommRing S] {υ : Type u_5} {T : Type u_6} [inst_1 : CommRing T] [inst_2 : Algebra S T]
  {a : PowerSeries S},
  PowerSeries.HasSubst a →
    ∀ {b : MvPowerSeries υ T} (hb : PowerSeries.HasSubst b), PowerSeries.HasSubst ((PowerSeries.substAlgHom hb) a)