{F : Type u_7} →
  {α : Type u_8} →
    {β : Type u_9} →
      [inst : NonUnitalNonAssocRing α] →
        [inst_1 : Semiring β] →
          [inst_2 : PartialOrder β] →
            [inst_3 : FunLike F α β] →
              {motive : RingNormClass F α β → Sort u} →
                (t : RingNormClass F α β) →
                  ([toRingSeminormClass : RingSeminormClass F α β] →
                      (eq_zero_of_map_eq_zero : ∀ (f : F) {a : α}, f a = 0 → a = 0) → motive ⋯) →
                    motive t