prove a specialisation of compile_val for a closure body

the hope is to prove a series of theorems, starting with this one, about
what happens when a function call is made, sorting out the requisite
invariants and hypotheses, to eventually get a theorem that relates a
source-level function call to a manually set-up bytecode machine about
to do a CallPtr.
remove some unnecessary specialisation and hypotheses from that theorem