∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] {f : M →+ N} (U : Set (M × Mᵃᵒᵖ))
  (y : AddUnits N) (motive : (∃ x, (↑x, AddOpposite.op ↑(-x)) ∈ U ∧ (AddUnits.map f) x = y) → Prop)
  (x : ∃ x, (↑x, AddOpposite.op ↑(-x)) ∈ U ∧ (AddUnits.map f) x = y),
  (∀ (x : AddUnits M) (hxV : (↑x, AddOpposite.op ↑(-x)) ∈ U) (hx : (AddUnits.map f) x = y), motive ⋯) → motive x