data Bool () where
    True  : Bool ()
    False : Bool ()

not x = case x of
    True => False
    False => True

even : Int -> Bool ()
even x = not (odd x)
odd x = not (even x)