'a,'b,'c:S, x:('a 
'b 'c), x@0:('a 'b), x@1:'a.
Thm* x(x@1,x@0(x@1)) = x(x@1,x@0(x@1))
'a,'b,'c:S.
Thm* all
Thm* (
f:'a 'b 'c. all
Thm* (
f:'a 'b 'c. (g:'a 'b. all(x:'a. equal(s(f,g,x),f(x,g(x))))))| Theorem | Name |
| 'a,'b,'c:S, x:('a 'b 'c), x@0:('a 'b), x@1:'a.
Thm* x(x@1,x@0(x@1)) = x(x@1,x@0(x@1)) | [s_thm] |
| cites the following: | |
| 'a,'b,'c:S.
Thm* all Thm* ( f:'a 'b 'c. all
Thm* ( f:'a 'b 'c. (g:'a 'b. all(x:'a. equal(s(f,g,x),f(x,g(x)))))) | [hs_thm] |