Make 'caseBool' parser use eliminator syntax.
Make 'caseBool' parser use eliminator syntax.

Also, added a nice error message for the motive part of the 'caseBool'
parse.

New syntax is

  caseBool (\ x -> m) t f b .

Actually, for true eliminator syntax, we would allow an arbitrary
function for the motive, i.e.

  caseBool m t f b .

However, the internal 'caseBool' primitive requires an lambda; we
could achieve this by eta-expanding the motive 'm', but that would
require fresh name generation, which I'll avoid for now.

(Technically, the 'caseBool' primitive requires the premise to a
function introduction, i.e. a

  C , Bool |- Type

instead of a

  C |- Bool -> Type ,

but we can recover this immediately from a lambda by inverting it;
indeed, the parser in this commit does just that).

spire/spire