== Formalization of normalization-by-evaluation for Martin Lof Type Theory with Universe.
== Pawel Wieczorek, University of Wroclaw, Poland
This package contains formalization of NBE for dependend type thoery in Martin-Lof style. Main goal of this
project is to provide certified normalizer and decision procedure for term/type equality.
Second goal is to provide well-written package, which could be easy modifiable by other people.
Package is written for Coq 8.4pl3 (February 2014).
>>> Type Theory