Implement proofs/simplification

[bn0367]

Long term goal.
Implement simplifying expressions, which goes hand in hand with proofs.

[bn0367]

Alright, turns out "simplification" is easy enough. Simplifies xor to (~p ^ q) v (p ^ ~q), but in general it simplifies. Proving will take a lot more work.