Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/a2415058e884fb275b52088ccc40369c]
nat : type.
z : nat.
s : nat -> nat.
id-nat : nat -> nat -> type.
id-nat/refl : {N:nat} id-nat N N.
plus : nat -> nat -> nat -> type.
plus/z : {N:nat} plus z N N.
plus/s : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus (s N1) N2 (s N3).
%solve 
plus (s (s (s z))) (s (s z)) N.
 OK
_ : plus (s (s (s z))) (s (s z)) (s (s (s (s (s z)))))
   = plus/s (plus/s (plus/s plus/z)).
[Closing file /home/www/twelf/hcode/a2415058e884fb275b52088ccc40369c]
%% OK %%