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).