When applied to a term-tactic pair (tm,tac), the function
PROVE attempts to prove the goal ?- tm, that is, the term tm
with no assumptions, using the tactic tac. If PROVE succeeds,
it returns the corresponding theorem A |- tm, where
the assumption list A may not be empty if the tactic is invalid;
PROVE has no inbuilt validity-checking.