prove last cheats in pmatch_enveq

compiler proofs now have no cheats.

for the main compiler theorem, the caveats in the theorem statement are:
  - assume the module environment is empty, and no modules are declared
  - assume termination in the semantics

(the other assumptions are about things being "closed" (no unbound
names), and about labels in the existing bytecode (e.g. no duplicates),
which I hope can be discharged in context)