LAWS.omap_get_put_same: law of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/LAWS.bend as LAWS
Lines 193-205 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=193&end_line=205

import Base
import bend-kit-collections@0.1.4.1/omap.bend as O

law omap_get_put_same:
  for ~K: Data
  for ~V: Data
  for ~cmp: K -> K -> Cmp
  for ~refl: @x: K -> {cmp(x, x) == EQ{} : Cmp}
  for ~eq: @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K}
  for ~flip: @x: K -> @y: K -> {cmp(y, x) == flip(cmp(x, y)) : Cmp}
  for ~trans: @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp}
  for m: O.OMap<K, V>
  for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool}
  for +k: K
  for +v: V
  {O.OMap.get(~K, ~V, ~cmp, O.OMap.put(~K, ~V, ~cmp, m, k, v), k) == Some{v} : Maybe<&2, V>}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=flip
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=searchtree
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=get_put_same
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap.get
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap.put