Proof Tree Representation Code to generate the whole proof tree, proof as program tree annotated by its types on all branches.