Adds theorem and proof construct

[nskh]

Replaces #1263.

In-progress PR to add a theorem keyword in the style of let-equals-in to Hazel.

Based on stepper-rewrites this time.

[nskh]

@Negabinary: I addressed your changes, should be ready for review. We can merge as-is, or discuss how to add in some way to invoke a stepper by adding a proof keyword here too.

[cyrus-]

theorem name = typ 
proof "serialized stepper data" 
in e

things we need in the typ syntax:

forall x -> ty
exists x : T -> typ.  [sigma types]
(x : typ) -> typ. [pi types]
   (syntactic sugar: forall x : T -> ty)
typ(typ). 
e1 = e2.  [equality types]

[cyrus-]

If we do the syntax as:

theorem name : typ 
proof e1
in e2

then this becomes just another let expression exactly -- that should be pretty straightforward to do so let's update this PR in that direction, then make another PR for adding the new type forms.

[cyrus-]

TODO:

• change sorting to theorem pat = exp in exp, which matches let expressions exactly
• have theorem behave exactly like a let expression everywhere else in the codebase
• at the type level, rename existing forall to type
• add new forall pat -> ty construct to types
• add {e1 = e2} form to types