{G : Type u_3} →
  [inst : AddGroup G] →
    {H K : AddSubgroup G} →
      {motive : H.IsFiniteRelIndex K → Sort u} →
        ((relIndex_ne_zero : H.relIndex K ≠ 0) → motive ⋯) → (t : H.IsFiniteRelIndex K) → motive t