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