law splice_same

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/map_insert.bend:109

import Base

109law splice_same:
110  for -V: Data
111  for d: V
112  for x: V
113  for rest: Map<&2, V>
114  for +p: Nat
115  for +key: String
116  {lookup(V, d, Map.ins.splice(&2, V, p, key, x, rest), key) == x : V}