∀ (carrier : Type u) [booleanRing : BooleanRing carrier] (carrier_1 : Type u) (booleanRing_1 : BooleanRing carrier_1),
  ({ carrier := carrier, booleanRing := booleanRing } = { carrier := carrier_1, booleanRing := booleanRing_1 }) =
    (carrier = carrier_1 ∧ booleanRing ≍ booleanRing_1)