Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/89987de02a9b26440a380e0127f9b222]
tp : type.
unit : tp.
arrow : tp -> tp -> tp.
exp : type.
* : exp.
lam : tp -> (exp -> exp) -> exp.
app : exp -> exp -> exp.
of : exp -> tp -> type.
of/star : of * unit.
of/app :
   {E2:exp} {T:tp} {E1:exp} {T':tp}
      of E2 T -> of E1 (arrow T T') -> of (app E1 E2) T.
of/lam :
   {T:tp} {E:exp -> exp} {T':tp}
      ({x:exp} of x T -> of (E x) T') -> of (lam T ([x:exp] E x)) (arrow T T').
_ :
   {X1:{x:exp} of x unit -> of x unit}
      of (lam unit ([x:exp] x)) (arrow unit unit)
   = [X1:{x:exp} of x unit -> of x unit] of/lam ([x:exp] [x1:of x unit] X1 x x1).
_ : of (lam unit ([x:exp] x)) (arrow unit unit)
   = of/lam ([x:exp] [d:of x unit] d).
value : exp -> type.
value/star : value *.
value/lam : {T:tp} {E:exp -> exp} value (lam T ([x:exp] E x)).
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' -> value E1 -> step (app E1 E2) (app E1 E2').
step/applam :
   {E2:exp} {T:tp} {E:exp -> exp}
      value E2 -> step (app (lam T ([x:exp] E x)) E2) (E E2).
preservation : {E:exp} {T:tp} {E':exp} of E T -> step E E' -> of E' T -> type.
%mode +{E:exp} +{T:tp} +{E':exp} +{D1:of E T} +{D2:step E E'} -{D3:of E' T}
   (preservation D1 D2 D3).
[Closing file /home/www/twelf/hcode/89987de02a9b26440a380e0127f9b222]
%% OK %%