no goals
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type ?u.373127
inst✝ : Monoid N
w : Word M
i : ι
⊢ ¬fstIdx w ≠ some i ↔ ¬∀ (l : (i : ι) × M i), l ∈ List.head? w.toList → i ≠ l.fst
simp [fstIdx]