Implement equality operator

[MasterOdin]

(= a b) or equals(a, b)

Allow for proofs of the form:

From A, A = B conclude B

1. A
2. A = B
3. Not(B)
4. B (from 1 and 2)
5. ⊥

✓