m,n:
. even(m+n) 
(even(m) even(n))
m:hnum. all(n:hnum. equal(even(add(m,n)),equal(even(m),even(n)))))| Theorem | Name |
| m,n:. even(m+n) (even(m) even(n)) | [even_add] |
| cites the following: | |
| m:hnum. all(n:hnum. equal(even(add(m,n)),equal(even(m),even(n))))) | [heven_add] |