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