∀ {R : Type u} [inst : Semiring R] (r : R → R → Prop) [inst_1 : StarRing R]
  (hr : ∀ (a b : R), r a b → r (star a) (star b)) (a a_1 : RingQuot r),
  a = a_1 → RingQuot.star'✝ r hr a = RingQuot.star'✝¹ r hr a_1