Prover usefulness

This improves the interaction between the REPL and the prover greatly. It also fixes #146.