∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : (i : ι) → DecidableEq (M i)] {i j : ι}
  (p : Monoid.CoprodI.Word.Pair M i) (m : M j),
  (⟨j, m⟩ ∈
        (if h : p.head = 1 then p.tail
          else { toList := ⟨i, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList) =
      (⟨j, m⟩ ∉ p.tail.toList ∧ (m = 1 ∨ ∀ (a : i = j), ¬m = a ▸ p.head)) →
    ¬p.head = 1 →
      ⟨j, m⟩ ∈
          (if h : p.head = 1 then p.tail
            else { toList := ⟨i, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList →
        i = j