Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Struct()
axiom()
cond()
define()
prove()
search()
simp()
BaseSolver
EProverTHFSolver
LeoIIISolver
MultiSolver
NanoCopISolver
SATSolver
TweeSolver
VampireSolver
VampireTHFSolver
ZipperpositionSolver
binpath()
collect_decls()
collect_sorts()
expr_to_smtlib()
expr_to_tptp()
funcdecl_smtlib()
install_solvers()
mangle_decl()
mangle_decl_smtlib()
run()
smtlib_datatypes()
sort_to_tptp()
run_aprove()
vs (list[ExprRef])
eqs (list[BoolRef])