no goals
p : ℕ
R : Type u_1
S : Type ?u.661694
T : Type ?u.661697
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type ?u.661712
β : Type ?u.661715
x y : 𝕎 R
⊢ WittVector.ghostFun (x + y) = WittVector.ghostFun x + WittVector.ghostFun y
ghost_fun_tac X 0 + X 1, ![x.coeff, y.coeff]