∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (motive : Finite ↥H ∧ H.FiniteIndex → Prop)
  (x : Finite ↥H ∧ H.FiniteIndex), (∀ (left : Finite ↥H) (right : H.FiniteIndex), motive ⋯) → motive x