Bool ::= False | True
Nat ::= O | S Nat
Maybe a ::= Nothing | Just a

Not :: Bool -> Bool
Not = False -> True
    | True -> False

Match :: _ -> _ -> Bool
Match a = a -> True
        | _ -> False

Pred ::= S (x : Nat) -> x