Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/174ce67dc7ad0ac4165cb5abb9b7169d]
exp : type.
abs : (exp -> exp) -> exp.
app : exp -> exp -> exp.
step : exp -> exp -> type.
step/app1 :
   {E1:exp} {E1':exp} {E2:exp} step E1 E1' -> step (app E1 E2) (app E1' E2).
step/app2 :
   {E2:exp} {E2':exp} {E1:exp} step E2 E2' -> step (app E1 E2) (app E1 E2').
step/appabs : {E:exp -> exp} {E':exp} step (app (abs ([x:exp] E x)) E') (E E').
[Closing file /home/www/twelf/hcode/174ce67dc7ad0ac4165cb5abb9b7169d]
%% OK %%