bool(2)

Tの定義．

T_DEF: `T = ((\x:bool. x) = (\x:bool. x))`
TRUTH: `|- T`
EQT_ELIM `ASM1 |- a = T` gives `ASM1 |- a`
EQT_INTRO `ASM1 |- a` gives `ASM1 |- a = T`

Fの定義．

F_DEF: `F = !t:bool. t`
NOT_DEF: `(~) = \t. t ==> F`
NOT_ELIM `ASM |- ~a` gives `ASM |- a ==> F`
NOT_INTRO `ASM |- a ==> F` gives `ASM |- ~a`
EQF_INTRO `ASM |- ~a` gives `ASM |- a = F`
EQF_ELIM `ASM |- a = F` gives `ASM |- ~a`
NEG_DISCH `a` `ASM,a |- F` gives `ASM |- ~a` (if the conclusion of the
          initial theorem is not F, then NEG_DISCH acts like DISCH)
CONTR `a` `ASM |- F` gives `ASM |- a`