q
p
x:A. B(x)
q
q Q Q
case0; 3 case1; 3 case2;
| Def | p q | [K_imp] | ||
| Def | p | [K_not] | ||
| Def | | [Three] | Three | |
| Def | x:A. B(x) | [all] | core | |
| Def | p q | [K_and] | ||
| Def | p q | [K_or] | ||
| Def | P & Q | [and] | core | |
| Def | P Q | [implies] | core | |
| Def | P Q | [or] | core | |
| Def | 3 | [Three_1] | Three | |
| Def | 3 | [Three_2] | Three | |
| Def | case x: 3 case0; 3 case1; 3 case2; | [Three_case] | Three | |
| Def | 3 | [Three_0] | Three |
About:
 |  |  |  |  |  |
 |  |  |
 |  |  |