Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/794ee6e76c6d196c62a7846e8228702b]
tp : type.
=> : tp -> tp -> tp.
%infix right 10 =>.
exp : tp -> type.
lam : {A:tp} {B:tp} (exp A -> exp B) -> exp (A => B).
app : {A:tp} {B:tp} exp (A => B) -> exp A -> exp B.
val : {A:tp} exp A -> type.
lam-val : {X1:tp} {X2:tp} {E:exp X1 -> exp X2} val (lam ([x:exp X1] E x)).
eval : {A:tp} exp A -> exp A -> type.
eval-lam :
   {X1:tp} {X2:tp} {E:exp X1 -> exp X2}
      eval (lam ([x:exp X1] E x)) (lam ([x:exp X1] E x)).
eval-app :
   {X1:tp} {X2:tp} {E1':exp X2 -> exp X1} {V2:exp X2} {V:exp X1} {E2:exp X2}
      {E1:exp (X2 => X1)}
      eval (E1' V2) V -> eval E2 V2 -> eval E1 (lam ([x:exp X2] E1' x))
         -> eval (app E1 E2) V.
[Closing file /home/www/twelf/hcode/794ee6e76c6d196c62a7846e8228702b]
%% OK %%