law singleton_get

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/lemmas/proofs/native_map.bend:93

import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend as NativeMap
import Base

93law singleton_get:
94  for -V: Data
95  for d: V
96  for k: String
97  for v: V
98  {Map.get(V, d, MLeaf{k, v}, k) == (MLeaf{k, v}, v) : Map<&2, V> & V}

Uses (10)

Used by (1)