Resolved some issue
Merge remote-tracking branch 'upstream/fomega' into fomega
Signal an error if an unknown term is fed into the type checker
Hint on the behaviour of the signature analysis
Variants and records are t. b. d.
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.
Some notes and debugging output
On the way to fix teh verificator
Rough fix of normalization axioms

We must augment parReduce instead of norm. parReduce must
also have a fall back for meta variables. This fall back must
not interfere with dynamic axioms.

A wrong let is now detected. A right let is accepted.
Cleanup and removed some debug output
Merge remote-tracking branch 'florian/fomega'