Add case to initial Env and levitate Branches
Fix Branches by making it a primitive.

Unfortunatley, functional types like Branches cannot be levitated at the moment.
Because our canonical syntax contains bindings, when we embed bound values (like
a motive argument) they must be wrapped in a lambda. Type checking of "case"
requires checking against a "Branches" argument, which must introduce one of
these lambda-wrapped motives.

One solution is to change the canonical syntax to mostly take function
argument rather than bindings, but this would make the syntax less
binding-safe.

The better solution would be to extend definitonal equality to
include eta.