WIP Primitives clean up (experimental)

[mkarup]

Clean up / refactor (WIP) PR for primitive operations.

The idea will be to move as much of the proof code for primitives as possible into LambdaANF_to_Wasm_primitives.v

Initial attempt will be to state lemmas only in terms of definitions from wasmcert, and then only require a small amount of lemmas to "glue" it together in the main proof file.

The current commits are very, very early stage, and not at all complete, and the approach may change.

Separate the proof code for primitive operations into a separate file:

The main theorem of LambdaANF_to_Wasm_correct.v now has an assumption that primitive operations reduce (primitive_operation_reduces), and the proof for this assumption has been moved to a new file LambdaANF_to_Wasm_primitives_correct.v.