Sorted.sort_count: law of bend-lawful-stdlib@0.1.0.0
Import: import bend-lawful-stdlib@0.1.0.0/src/sorted.bend as Sorted
Lines 215-222 of bend-lawful-stdlib@0.1.0.0/src/sorted.bend: https://jend.leeeet.dev/read.txt?path=bend-lawful-stdlib@0.1.0.0/src/sorted.bend&start_line=215&end_line=222

import Base
import bend-lawful-stdlib@0.1.0.0/src/class.bend as C

# sort keeps every element's count.
law sort_count:
  for ~A: Data
  for ~o: C.Ord<A>
  for ~eq: A -> A -> Bool
  for +y: A
  for xs: List<&2, A>
  {count(~A, ~eq, y, xs) == count(~A, ~eq, y, sort(~A, ~o, xs)) : Nat}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Ord
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/sorted.bend&name=bump
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/sorted.bend&name=count
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/sorted.bend&name=insert_count
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/sorted.bend&name=sort