Started verification of typing rules

* Extensions to norm and typeEqProper to handle meta-variables correctly.
* Additions to the judgment implementations to hook in dynamically
  activated axioms.
* Transfer of Sebastians draft to the Fomega setting.

Not completed yet.