∀ (S : Set ℕ) (B : Type u_1) [inst : CommRing B] (x : B) (motive : x ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} → Prop)
  (x_1 : x ∈ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}),
  (∀ (n : ℕ) (hn : n ∈ S) (h1 : n ≠ 0) (h2 : x ^ n = 1), motive ⋯) → motive x_1