minor: make cases disjoint
first steps towards a proof debugger
add a flag for ok derivation or not
first stab at showing derivation trees for debugging
colors