Lessons Learned
Tactic steps correspond approximately with human inference steps.
Some proof content is part of the general mathematical knowledge of Nuprl and is not included in the proof.
There is information which is needed to communicate correctness of a proof to a person which is not needed by Nuprl to determine truth.