move Opaque statements out of theorem proofs
move Opaque statements out of theorem proofs

this allows coqide to run with more parallelism

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl