no goals
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.609541
inst✝ : Monoid N
i j k l : ι
w₁ : NeWord M i j
hne : j ≠ k
w₂ : NeWord M k l
⊢ prod (append w₁ hne w₂) = prod w₁ * prod w₂
simp [toWord, prod, Word.prod]