{ι : Type u_1} →
  {G : ι → Type u_2} →
    [inst : (i : ι) → Group (G i)] →
      (motive : (x x_1 : ι) → Monoid.CoprodI.NeWord G x x_1 → Sort u_3) →
        (x x_1 : ι) →
          (x_2 : Monoid.CoprodI.NeWord G x x_1) →
            ((x : ι) → (x_3 : G x) → (h : x_3 ≠ 1) → motive x x (Monoid.CoprodI.NeWord.singleton x_3 h)) →
              ((x x_3 j k : ι) →
                  (w₁ : Monoid.CoprodI.NeWord G x j) →
                    (h : j ≠ k) → (w₂ : Monoid.CoprodI.NeWord G k x_3) → motive x x_3 (w₁.append h w₂)) →
                motive x x_1 x_2