WIP: Beginning of import of the evaluation function

We start to import the evaluation function from OCaml and make some proofs. Main changes so far:

• import the full AST without annotations on the GADTs;
• update the proofs on the AST without GADT annotations;
• import a beginning of the evaluation function;
• use some Obj_magic to type-check without GADT annotations;
• use the plugin coq-typing-flags to accept the termination of the evaluation function (breaks compatibility with Coq 8.10);
• write the beginning of the proof of equivalence with the Mi-Cho-Coq evaluation.