law singleton_get
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend as NativeMapimport 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}