{R : Type u_1} →
  [inst : Ring R] →
    {motive : RingCone R → Sort u} →
      (t : RingCone R) →
        ((toSubsemiring : Subsemiring R) →
            (eq_zero_of_mem_of_neg_mem' : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0) →
              motive { toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem' }) →
          motive t