:let N = (R : *) -> R -> (R -> R) -> R
:let Nat = Ty N

:let zero : Nat = Con N (\(R : *) (z : R) (s : R -> R) -> z)
:let suc (n : Nat) : Nat = Con N (\(R : *) (z : R) (s : R -> R) -> s (unCon N n R z s))

:let Pair (A B : *) = Ty ((R : *) -> (A -> B -> R) -> R)

:{:let
  pair (A B : *) (x : A) (y : B) : Pair A B
       = Con ((R : *) -> (A -> B -> R) -> R)
             (\(R : *) (f : A -> B -> R) -> f x y)
:}

:{:let
  uncurry (A B R : *) (f : A -> B -> R) (p : Pair A B) : R
        = unCon ((R : *) -> (A -> B -> R) -> R) p R f
:}