Fix checker treatment of inductives using subst_instances instead of subst_univs_levels.
Remove unused substitution functions in checker.
Fix checking of constants in checker. Prelude can now be checked.
Fix checker to handle projections with eta and universe polymorphism correctly.
Fix checker to handle projections with eta and universe polymorphism correctly,
simplifying conversion code.
Cleanup code for looking up projection bodies.
Remove debug printing code
Fix bug #3584, elaborating pattern-matching on primitive records to the
use of projections.