∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R) (n : ℕ),
  (MvPolynomial.aeval x.coeff) (WittVector.verschiebungPoly n) = (WittVector.verschiebung x).coeff n