Simplify casl formulas and CCC proof obligations

When collecting nested conditions in conditionAxiom (that was not recursive before) the formula is already simplified during construction.

I think this makes sense although `simplifyFormula` is called later on (and repeats certain checks).
(Calling simplifyFormula on all leaves is more work.)