Implement NbE for lambda calculus with conditionals (see #50).
Implement NbE for lambda calculus with conditionals (see #50).

This version is simpler than the code in NormalizationByEvaluation
in the following ways:

 - Instead of supporting arbitrary base types and constants,
   bool, true, false, and if are hard-coded.

 - Instead of supporting arbitrary Kripke structures,
   metacircular evaluation and symbolic evaluation are hard-coded.

Old-commit-hash: d25aa0871f3efecd4932029a007775f4c22568fb

inc-lc/ilc-agda