LAWS.order_string_refl: law of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/LAWS.bend as LAWS
Lines 224-229 of bend-kit-collections@0.1.4.1/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&start_line=224&end_line=229

import Base
import bend-kit-collections@0.1.4.1/order.bend as Order

# Order.string is a total order with EQ meaning equal strings: it meets the
# refl, eq, flip and trans facts that the OMap laws above take. It answers for
# every pair, so it is total; flip makes it antisymmetric.
law order_string_refl:
  for x: String
  {Order.string(x, x) == EQ{} : Cmp}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.cmp
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=ucmp_refl
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/order.bend&name=string
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/order.bend&name=string.fin