'b,'a:S, x:('a 
'b).
Thm* (
x:'b. x) o x = x 
('a 'b) & x o (x:'a. x) = x ('a 'b)'b,'a:S. all(f:'a 'b. and(equal(o(i,f),f),equal(o(f,i),f)))| Theorem | Name |
| 'b,'a:S, x:('a 'b).
Thm* ( x:'b. x) o x = x ('a 'b) & x o (x:'a. x) = x ('a 'b) | [i_o_id] |
| cites the following: | |
| 'b,'a:S. all(f:'a 'b. and(equal(o(i,f),f),equal(o(f,i),f))) | [hi_o_id] |