∀ {carrier : Type u_1} {str : Order.Frame carrier} {carrier_1 : Type u_1} {str_1 : Order.Frame carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1