Nat_Polytype : *p
 = (Data:*) -> (Succ:Data -> Data) -> (Zero:Data) -> Data
Nat : *m  = Monotype Nat_Polytype
zero : Nat = (monotype Nat_Polytype) (λ(Data:*) (Succ:Data -> Data) (Zero:Data) -> Zero)
succ (n:Nat) : Nat
 = monotype Nat_Polytype
   (λ(Data:*) (Succ:Data -> Data) (Zero:Data) ->
     Succ (polytype Nat_Polytype n Data Succ Zero))
one   : Nat = succ zero
two   : Nat = succ one
three : Nat = succ two
plus (n:Nat) (m:Nat) : Nat
 = monotype Nat_Polytype
   (λ(Data:*) (Succ:Data -> Data) (Zero:Data) ->
     polytype Nat_Polytype n Data Succ (polytype Nat_Polytype m Data Succ Zero))
mult (n:Nat) (m:Nat) : Nat
 = monotype Nat_Polytype
   (λ(Data:*) (Succ:Data -> Data) (Zero:Data) ->
     polytype Nat_Polytype n Data (polytype Nat_Polytype m Data Succ) Zero)