    Variable names may clash in the printed representations.  (Although the variable "names" used internally are Java object
references, and so shouldn't clash.)

in the prover:
    The "Intro" rule is broken.  The problem is almost certainly in proof.prove.Goal, which needs rethinking. 
    No attempt is made to inhabit records (Sigma types.) 
    This probably should use iterative deepening, instead of storing the entire proof tree up to some depth in memory. 


