∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S} (ha : PowerSeries.HasSubst a), (PowerSeries.substAlgHom ha) PowerSeries.X = a