∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (x : M)
  (motive : x ∈ Submonoid.map (MulEquiv.refl M).toMonoidHom S → Prop)
  (x_1 : x ∈ Submonoid.map (MulEquiv.refl M).toMonoidHom S),
  (∀ (w : M) (hy : w ∈ ↑S) (h : (MulEquiv.refl M).toMonoidHom w = x), motive ⋯) → motive x_1