case0; 3
case1; 3
case2;
x:A. B(x)
}
j < kB
A
| Def | 3 | [three] | ||
| Def | case x: 3 case0; 3 case1; 3 case2; | [Three_case] | ||
| Def | True | [true] | core | |
| Def | | [Three] | ||
| Def | x:A. B(x) | [all] | core | |
| Def | 3 | [Three_1] | ||
| Def | 3 | [Three_0] | ||
| Def | Dec(P) | [decidable] | core | |
| Def | {i..j} | [int_seg] | int 1 | |
| Def | i j < k | [lelt] | int 1 | |
| Def | AB | [le] | core | |
| Def | A | [not] | core | |
| Def | 3 | [Three_2] | ||
| Def | Unit | [unit] | core | |
| Def | | [it] | core |
About:
 |  |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |  |  |