Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/1923cd7f9f9c84be02f0b324ae90e229]
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/twelfwiki/code/1923cd7f9f9c84be02f0b324ae90e229]
%% OK %%