law put_go_bridge

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/lemmas/proofs/map_bridge.bend:190

import Base

190law put_go_bridge:
191  for -a: Quant
192  for -V: Kind(a)
193    for x: V
194for +p: Nat
195  for lo: Map<a, V>
196  for hi: Map<a, V>
197  for kb: String & Bool
198  {Map.put.go(a, V, MNode{p, lo, hi}, x, kb) == put_bit(a, V, x, p, lo, hi, kb) : Map<a, V>}