initial thoughts on Opapp_compiled theorem

I want this theorem to say that if you evaluate an expression in the
source language, and that expression happens to be the body of a
closure, and there's a refinement of that closure on the bytecode stack
(and of the argument too), then you can make a call in the bytecode and
get a refinement of the result. This means having to go through all the
layers of refinements from the closure down to the bytecode closure,
which is pretty delicate, or at least complex/confusing. In part because
there are existential quantifiers along the way.