∀ {G : Type u_1} [inst : Group G] {motive : (a : Subgroup G) → a.IsSubnormal → Prop} {a : Subgroup G}
  (t : a.IsSubnormal),
  motive ⊤ ⋯ →
    (∀ (H K : Subgroup G) (h_le : H ≤ K) (hSubn : K.IsSubnormal) (hN : (H.subgroupOf K).Normal), motive H ⋯) →
      motive a t