Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/9e4a23b8db7db45fd07d84f69b739cf9]
t : type.
nat : type = (t -> t) -> t -> t.
0 : (t -> t) -> t -> t = [s:t -> t] [z:t] z.
s : ((t -> t) -> t -> t) -> (t -> t) -> t -> t
   = [n:(t -> t) -> t -> t] [s:t -> t] [z:t] s (n ([x:t] s x) z).
+ : ((t -> t) -> t -> t) -> ((t -> t) -> t -> t) -> (t -> t) -> t -> t
   = [n:(t -> t) -> t -> t] [m:(t -> t) -> t -> t] [s1:t -> t] [z:t]
        n ([x:t] s1 x) (m ([x:t] s1 x) z).
%infix right 10 +.
item : type.
list : ((t -> t) -> t -> t) -> type.
nil : list ([x:t -> t] [x1:t] x1).
cons :
   {N:(t -> t) -> t -> t}
      item -> list ([x:t -> t] [x1:t] N ([x2:t] x x2) x1)
         -> list ([x:t -> t] [x1:t] x (N ([x2:t] x x2) x1)).
append :
   {M:(t -> t) -> t -> t} {N:(t -> t) -> t -> t}
      list ([x:t -> t] [x1:t] M ([x2:t] x x2) x1)
         -> list ([x:t -> t] [x1:t] N ([x2:t] x x2) x1)
         -> list ([x:t -> t] [x1:t] M ([x2:t] x x2) (N ([x2:t] x x2) x1))
         -> type.
append_nil :
   {X1:(t -> t) -> t -> t} {L:list ([x:t -> t] [x1:t] X1 x x1)} append nil L L.
append_cons :
   {X1:(t -> t) -> t -> t} {X2:(t -> t) -> t -> t}
      {L1:list ([x:t -> t] [x1:t] X1 x x1)}
      {L2:list ([x:t -> t] [x1:t] X2 x x1)}
      {L3:list ([x:t -> t] [x1:t] X1 x (X2 x x1))} {T:item}
      append L1 L2 L3 -> append (cons T L1) L2 (cons T L3).
[Closing file /home/www/twelf/hcode/9e4a23b8db7db45fd07d84f69b739cf9]
%% OK %%