from abstract back to concrete (wip)

wf-val with respect to runtime env H.

TODO:
- extend and restrict wf-val
- uniqueness in proof of lookup-sel-safe