∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)]
  (motive : (x x_1 : ι) → Monoid.CoprodI.NeWord M x x_1 → Sort u_3) (x x_1 : ι) (x_2 : Monoid.CoprodI.NeWord M x x_1)
  (h_1 : (i : ι) → (x : M i) → (a : x ≠ 1) → motive i i (Monoid.CoprodI.NeWord.singleton x a))
  (h_2 :
    (x x_3 j k : ι) →
      (w₁ : Monoid.CoprodI.NeWord M x j) →
        (_hne : j ≠ k) → (w₂ : Monoid.CoprodI.NeWord M k x_3) → motive x x_3 (w₁.append _hne w₂))
  (x_3 x_4 j k : ι) (w₁ : Monoid.CoprodI.NeWord M x_3 j) (_hne : j ≠ k) (w₂ : Monoid.CoprodI.NeWord M k x_4),
  x = x_3 →
    x_1 = x_4 →
      x_2 ≍ w₁.append _hne w₂ →
        (match x, x_1, x_2 with
          | i, .(i), Monoid.CoprodI.NeWord.singleton x a => h_1 i x a
          | x, x_5, w₁.append _hne w₂ => h_2 x x_5 j k w₁ _hne w₂) ≍
          h_2 x_3 x_4 j k w₁ _hne w₂