I already finished adding proof (including first-order) terms to
prover.pl; I still need to finish them for proverD.pl.

    I'd like to explore adding support for equality theories.  Maybe I
should just support a FIXED equality theory (a rewrite system): theorem
proving modulo a fixed equality theory.

    Alternatively, coding induction would be interesting.

    Another possibility is to aim for a "canonical" intuitionistic
prover that is clean enough to release widely.  If that's my aim, I'd
like to have a code walk through with someone else.