{ι : 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) →
            ((i : ι) → (x : M i) → (a : x ≠ 1) → motive i i (Monoid.CoprodI.NeWord.singleton x a)) →
              ((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₂)) →
                motive x x_1 x_2