{R : Type u} →
  [inst : NonAssocSemiring R] →
    {motive : Subsemiring R → Sort u_1} →
      (t : Subsemiring R) →
        ((toSubmonoid : Submonoid R) →
            (add_mem' : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier) →
              (zero_mem' : 0 ∈ toSubmonoid.carrier) →
                motive { toSubmonoid := toSubmonoid, add_mem' := add_mem', zero_mem' := zero_mem' }) →
          motive t