∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {S : Type u_2} [inst_2 : Semiring S]
  (x : S →+* WittVector p R) (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂),
  (TruncatedWittVector.truncate hk).comp (↑⟨fun k => (WittVector.truncate k).comp x, ⋯⟩ k₂) =
    ↑⟨fun k => (WittVector.truncate k).comp x, ⋯⟩ k₁