Draft: use SProp for well-formedness condition in Pmap and gmap
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).