∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : IsAlgClosed k] {a₁ : WittVector p k},
  a₁.coeff 0 ≠ 0 →
    ∀ (a₂ : WittVector p k),
      WittVector.RecursionBase.solution p a₁ a₂ ^ p * a₁.coeff 0 =
        WittVector.RecursionBase.solution p a₁ a₂ * a₂.coeff 0