∀ {p : ℕ} {f : ⦃R : Type u_2⦄ → [CommRing R] → WittVector p R → WittVector p R → WittVector p R},
  (∃ φ,
      ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : WittVector p R),
        (f x y).coeff = fun n => WittVector.peval (φ n) ![x.coeff, y.coeff]) →
    WittVector.IsPoly₂ p f