Add proofsearch tactic, with :ps at the REPL

At the moment, just invokes 'trivial'. There is a corresponding vim
command, \o, which invokes this and prints the result.