module nat where
  
data Nat : Set where
  O : Nat
  S : Nat -> Nat