Better naming for lifting canonically vs. structurally

[phlegmaticprogrammer]

Using true and false to distinguish between the two is just unreadable. So instead of lift(t, true) one should be able to just write lift! t, and similarly get rid of the nil / false / true thing in the theorem statement.

[phlegmaticprogrammer]

I got rid of the prefix destruct operator ! m which would work only on values which are custom constructors with an argument. Instead I introduced the postfix bang operator x ! which works differently depending on what x is. If x is a custom constructor applied to an argument, then x! is the argument. If x is a non-negative integer, then x! is just the factorial function. If x is nil, then the result is the new value nil! which just as nil has type Nil. If x is the native function lift, then the result is the native function liftstructurally.

The lift and liftstructurally take either a term or a theorem and lift canonically or in a way which preserves the structure, respectively.

Theorem now takes not anymore nil, true or false instead of a term literal, but only nil or nil!, and lifts canonically or structure preserving, respectively.