Dependent Types

WTy2 features dependent record and function types.

TODO (should start with low level definitions of dependent cons/telescopes and dependent function arrow)