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)