{ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} →
              {motive : Monoid.PushoutI.NormalWord d → Sort u} →
                (t : Monoid.PushoutI.NormalWord d) →
                  ((toWord : Monoid.CoprodI.Word G) →
                      (head : H) →
                        (normalized : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ toWord.toList → g ∈ d.set i) →
                          motive { toWord := toWord, head := head, normalized := normalized }) →
                    motive t