Remove Formula

[N1ark]

Partial Changelog:

• Remove Formula.t, using Expr.t anywhere it was used:
  The only difference at this point was a slightly different AST and the fact an Expr.t is not always a boolean expression, but it's not actually that big of a deal it seems.
  The biggest downside I got so far is that it's slightly more verbose: Eq (e1, e2) becomes BinOp (e1, Equals, e2), Not f becomes UnOp (Not, e), etc.
• Add patterns from reduce_formula into reduce_lexpr, cleaning up a bit, and remove reduce_formula
  There are a few rules that I removed, as they do not seem to stop the tests from passing and they caused errors after the merge -- I'll highlight these in the PR, to see if I'm correct in removing them.
• BinOp: rename BAnd → And, BOr → Or, BImpl → Impl, SLessThan → StrLess, BSetMem → SetMem, BSetSub → SetSub
• UnOp: rename UNot → Not, add IsInt from Formula
• Rename all symbolic infix operators (#==, #<, #&&...) to remove the hash, becoming ==, <, etc. This deeply embeds the Expr operators which I found nicer and also means the operators actually have different precedence! Because all operators starting with # have the same precedence which made using them annoying due to parenthesis.
• For GIL I didn't remove any of the existing syntax, but all Formula now compile as Expr, meaning that some operators have two equivalent symbols (eg. = and ==, <# and <, /\ and &&, --e-- and -e-...)
  The only difference is that pure formulae must be enclosed in parenthesis, and all other assertions must not be in parenthesis, ie. pred isTrue(+b: Boolean): b = true; must become pred isTrue(+b: Boolean): (b = true);. This is to allow distinguishing the assertion * operator from the expression's multiplication. (In reality this change only affected a handful of definitions).
• Remove the types vt, st and action_ret from the signature of the type SMemory, since their value was already set anyways (I think this doesn't change anything about the module type?) by using type _ := _ instead.

[NatKarmios]

A big'un! Looks fine overall, nice stuff.
Happy to merge once comments are resolved :)