MapInsert.insertion_same: law of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend as MapInsert
Lines 163-173 of bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend&start_line=163&end_line=173

import Base

# This actual native insertion law needs no well-formedness assumption: querying
# the new key follows the same bits used to choose its newly inserted leaf.
# Other-key preservation DOES require valid discriminator/difference properties.
law insertion_same:
  for -V: Data
  for +d: V
  for m: Map<&2, V>
  for +key: String
  for +x: V
  for +p: Nat
  {lookup(V, d, Map.ins(&2, V, m, key, x, p), key) == x : V}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Map
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Map.ins
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_bridge.bend&name=ins_if
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_bridge.bend&name=ins_node
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend&name=insertion_branch_same
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend&name=leaf_same
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend&name=lookup
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend&name=splice_same