Thm* 
Alph,St:Type, C:NComp(Alph;St). |C| 
Alph*
"?" ; h.t h
Thm* A:Type, l:A*. ||l||
1 
hd(l) A
Thm* A:Type, B:(A
Type), p:a:A
B(a). 2of(p) B(1of(p))
| nd_comp_car |
Def |C| == 2of(hd(C))
Thm* |
| hd |
Def hd(l) == Case of l; nil "?" ; h.t h
Thm* |
| pi2 |
Def 2of(t) == t.2
Thm* |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |