∀ {R : Type u_1} [inst : CommRing R] {μ : R} (motive : ↑{x | ∃ n, μ - 2 * ↑n = x} → Prop)
  (x : ↑{x | ∃ n, μ - 2 * ↑n = x}), (∀ (r : R) (hr : r ∈ {x | ∃ n, μ - 2 * ↑n = x}), motive ⟨r, hr⟩) → motive x