m,n,x:
. m+x = n+x 
m = nThm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. all
Thm* (
m:hnum. (n:hnum. (p:hnum. equal(equal(add(m,p),add(n,p)),equal(m,n)))))| Theorem | Name |
| m,n,x:. m+x = n+x m = n | [eq_mono_add_eq] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. all
Thm* ( m:hnum. (n:hnum. (p:hnum. equal(equal(add(m,p),add(n,p)),equal(m,n))))) | [heq_mono_add_eq] |