Collapse adjacent binders of the same quantifier
Improve error message when 'apply' has the wrong number of arguments
Allow case analysis on 'true' and 'false'
Fix bug in instantiation of 'with' variables
Remove spurious ^Ms
Restore some missing commits from agacek from earlier this year
Adding free <= and => to spec logic.

Also starting to add &. It is parsed and typechecked, but reasoning on it
is currently incorrect. There is no support for case splitting when
encountering a focused conjunction.