{M : Type u_3} →
  [inst : MulOneClass M] →
    {motive : Submonoid M → Sort u} →
      ((toSubsemigroup : Subsemigroup M) →
          (one_mem' : 1 ∈ toSubsemigroup.carrier) → motive { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' }) →
        (t : Submonoid M) → motive t