module Ord where

data Nat : Set where
  Z : Nat
  S : Nat -> Nat


data Ord : Set  where
  z : Ord
  lim : (Nat -> Ord) -> Ord

zp  : Ord -> Ord
zp z = z
zp (lim f) = lim (\x -> zp (f x))