law ins_splice_bridge

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/map_bridge.bend:294

import Base

294law ins_splice_bridge:
295  for -a: Quant
296  for -V: Kind(a)
297  for +q: Nat
298  for lo: Map<a, V>
299  for hi: Map<a, V>
300  for x: V
301  for +p: Nat
302  for key: String
303  for kb: String & Bool
304  for hk: {routed_key(kb) == key : String}
305  {Map.ins.go(a, V, MNode{q, lo, hi}, x, p, kb, False{}) == Map.ins.splice(a, V, p, key, x, MNode{q, lo, hi}) : Map<a, V>}