no goals
p : ℕ
R : Type ?u.284123
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
p' : ℕ
R' : Type u_1
x y : WittVector p' R'
i : Fin 2
⊢ (Matrix.vecCons x ![y] i).coeff = Matrix.vecCons x.coeff ![y.coeff] i
fin_cases i <;> simp