Mr Solver support for monadic Cryptol specs

[eddywestbrook]

This PR makes it possible for Mr Solver to work on specifications extracted from Cryptol. This required the following changes:

• Added the cryptol_add_prim and cryptol_add_prim_type SAW script commands for specifying the translations of Cryptol primitives and primitive types, respectively
• Changed monadification to add a macro for the either elimination function;
• Changed monadification so that functions not in the macro table with semi-pure types get monadified to themselves;
• Changed the implementation of assertFiniteM in the CryptolM SAW core module to use a Maybe type;
• Added support to Mr Solver for maybe eliminators over isFinite proofs;
• Added the mrNormOpenTerm function to Mr Solver and changed Mr Solver to use it instead of scWhnf to normalize terms with data type assumptions; and
• Put all these pieces together in a new test in linked_list_mr_solver.saw that uses Mr Solver to prove that is_elem refines a cryptol version of its specification

[m-yac]

LGTM!