fixed parellel reduction for terms containing metavars
added last type normalization rules and extended ADT tree example
added verification procedure for kind normalization rules