{G : Type u_1} →
  [inst : AddGroup G] →
    {motive : FiniteIndexNormalAddSubgroup G → Sort u} →
      ((toAddSubgroup : AddSubgroup G) →
          (isNormal' : toAddSubgroup.Normal) →
            (isFiniteIndex' : toAddSubgroup.FiniteIndex) →
              motive { toAddSubgroup := toAddSubgroup, isNormal' := isNormal', isFiniteIndex' := isFiniteIndex' }) →
        (t : FiniteIndexNormalAddSubgroup G) → motive t