defn nat : prop
   | zero = nat
   | succ = nat -> nat

defn even : nat -> prop
   | even/zero = even zero
   | even/odd = [N : nat] odd N -> even (succ N)

defn odd : nat -> prop
   | odd/zero = odd (succ zero)
   | odd/even = [N] even N -> odd (succ N)


defn funny : [N ] odd N -> prop
   | funnyodd = funny (<N> N) (odd/even zero even/zero)