Library MetaCoq.Checker.MetaTheory

The subject reduction property of the system. We comment this as otherwise extraction can produce "axioms to be realized" values that make extracted code useless, as type are in Type.

Weak Normalization: every term has a normal form