Given the trivial proof for EX x. x >' 0' by using the axiom 1' >' 0', is
there a way to see by which term x is instantiated (by 1' in this case)? Can
this be done in PG? If not, how can this be done in ML?