Closed requested to merge tchajed/stdpp:sprop-gmap into master
Proof of concept for #85. I'm not sure the reduction behavior is actually what we want, but I was able to get a lookup on a concrete map to reduce using only
simpl (ordinarily you can get this to work with
vm_compute, which breaks the opacity of proofs).