Justifications

There are two types of justifications.

Computational Justifications

  These indicate precise applications of the forward and reverse direct computation rules  . They are comparatively very fast and generate no well formedness subgoals. The rewrite package uses these whenever possible.

Tactic Justifications

  These are more generally applicable. Extensive use is made of lemmas, and many well formedness subgoals are generated.