%%% Arithmetic types
%%% Author: Brigitte Pientka

nat : type.				%name nat X.
z : nat.
s : nat -> nat.

nt : nat -> type.			%name nt N.
nt_z : nt z.
nt_s : nt (s X) <- nt X.