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.