Heap.Heap.size.push: law of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/heap.bend as Heap
Lines 118-123 of bend-kit-collections@0.1.4.1/heap.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/heap.bend&start_line=118&end_line=123

import Base

# LAW: a push adds one to the size
law Heap.size.push:
  for -x: U32
  for  h: Heap<U32>
  {Heap.size(U32, Heap.push(~U32, ~U32.is_le, x, h))
   == 1n+Heap.size(U32, h) : Nat}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/heap.bend&name=Heap
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/heap.bend&name=Heap.push
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/heap.bend&name=Heap.size