∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) (x : M)
  (motive : x ∈ AddSubmonoid.map (AddMonoidHom.id M) S → Prop) (x_1 : x ∈ AddSubmonoid.map (AddMonoidHom.id M) S),
  (∀ (h : x ∈ ↑S), motive ⋯) → motive x_1