This function would probably be cleaner if we write it using some dispatching. That is, each object has a `_to_nnf` method, which rewrites the negation itself (top-level only) as a non-negated, and this function takes care of recursively calling it. For instance, `Implies(x, y)._to_nnf()` would return `And(x, Not(y))`. Top-level only because this method would handle the recursion.  

Let me know if that makes sense.