∀ {G : Type u_1} [hG : Group G] (motive : NormalizerCondition G → Subgroup G → Prop) (x : NormalizerCondition G)
  (x_1 : Subgroup G), (∀ (h : NormalizerCondition G) (H : Subgroup G), motive h H) → motive x x_1