Small optimizations for equality and comparisons using physical eq.
Interactive SL prover mode now functional for testing.
Improvements on pretty-printing mainly for interactive use.
Small bugfix for satisfiability checker front-end.
SL prover now makes explicit substitution and weakening steps so that
back-linking only occurs between syntactically identical sequents.