Set up test values. Make checkLevels catch illegal derivations. Make implication introduction always use first and last lines of current subproof. Fix subproof exit. Fix mistakes in andElimination and orElimination.