∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (a b : ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)) (motive : a ≈ b → Prop) (x : a ≈ b),
  (∀ (u : ↥(NumberField.Units.torsion K)) (hu : (fun m => m • b) u = a), motive ⋯) → motive x