Make case a primitive instead of elimTag
Get rid of "if" in examples.

This in preperation for making Expr call elims from Environment.
Revert "Get rid of "if" in examples."

This reverts commit 5aabe24f05e45ac006550f0bfc6fa8c31c1541cc.
Create initial evironment.

This is the beginning of the migration away from type checking expressions as much as possible.
Add elimBool to initEnv
Specialize List to Enum
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.
Add El to initial environment, and rename it to "Func"
Add elimDesc

swagerino al pacino
Start implementing Darkwing's Derived file, starting with curryFunc.
Yay!
Update Fix to include datatype parameters, make Fix nominal, and add it to the initial env.
Add Hyps
Add prove