bit more compile_call_val
prove compile_call_val

(but not sure if its assumptions are too strong)
prove compile_decs_from_empty to better match the thing actually eval'ed

keep compile_decs_wrap_from_empty around too in case we want to use that..
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.
verification of repl_fun with label compilation
translator now supports FUNION
reduce cheats about bc_eval and strip labels

reduced to knowing that you can unstrip labels, and that strip_labels is
idempotent...
Merge remote-tracking branch 'origin/master' into tup+eq

Conflicts:
	impl_proofs/Holmakefile
	impl_proofs/replCorrectScript.sml
Remove a type that isn't around anymore