∀ {K : Type u_1} [inst : Field K] {I : Ideal (NumberField.RingOfIntegers K)} (n : ℕ)
  (motive : (x : ↥(rootsOfUnity n (NumberField.RingOfIntegers K))) → (I.rootsOfUnityMapQuot n) x = 1 → Prop)
  (x : ↥(rootsOfUnity n (NumberField.RingOfIntegers K))) (h : (I.rootsOfUnityMapQuot n) x = 1),
  (∀ (ζ : (NumberField.RingOfIntegers K)ˣ) (hζ : ζ ∈ rootsOfUnity n (NumberField.RingOfIntegers K))
      (h : (I.rootsOfUnityMapQuot n) ⟨ζ, hζ⟩ = 1), motive ⟨ζ, hζ⟩ h) →
    motive x h