Support for printing proofs for a given instance of Ev.
Remove outdated TODOs
Now from boole import * will import all the necessary definitions from prelude and terms. unif and tactics are imported by default.