Implement equality operator #6
Description
(= a b) or equals(a, b)
Allow for proofs of the form:
From A, A = B conclude B
- A
- A = B
- Not(B)
- B (from 1 and 2)
- ⊥
✓
{{ message }}
(= a b) or equals(a, b)
Allow for proofs of the form:
From A, A = B conclude B
✓