|
type bot
|
|
|
|
type top
|
|
| u : top
|
|
|
|
type bad
|
|
| b : (top → bad → bot) → bad
|
|
|
|
-- TArr (TArr top (TArr bad bot)) bad
|
|
|
|
getBad : bad → (top → bad → bot)
|
|
:= rec[bad] (λx. x)
|
|
|
|
uBad : top → bad → bot
|
|
:= λu b. (getBad b) u b
|
|
|
|
bBad : bad → bot
|
|
:= λb. (getBad b) u b
|
|
|
|
veryBad : bot
|
|
:= bBad (b uBad)
|