| | Who Cites K not? |
|
| K_not | Def   p == case p: 3  3 ; 3 3; 3 3; |
| | | Thm*  p: . p  |
|
| Three | Def == Unit+Unit+Unit |
| | | Thm* Type |
|
| Three_1 | Def 3 == inr(inl( )) |
| | | Thm* 3 |
|
| Three_2 | Def 3 == inr(inr()) |
| | | Thm* 3 |
|
| Three_0 | Def 3 == inl() |
| | | Thm* 3 |
|
| Three_case | Def case x: 3 case0; 3 case1; 3 case2; == InjCase(x; zero. case0; one_or_two. InjCase(one_or_two; one. case1; two. case2)) |
| | | Thm* t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''. case 3: 3 c; 3 c'; 3 c''; t |
| | | Thm* t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''. case 3: 3 c'; 3 c''; 3 c; t'' |
| | | Thm* t:Type{i}, t':Type{j}, t'':Type{k}, c:t, c':t', c'':t''. case 3: 3 c; 3 c'; 3 c''; t'' |
