Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/3e16e789fef6385b35884575bc350848]
tp : type.
=> : tp -> tp -> tp.
%infix right 10 =>.
stlc_sort : type.
val : stlc_sort.
non-val : stlc_sort.
exp : stlc_sort -> tp -> type.
lam : {A:tp} {S:stlc_sort} {B:tp} (exp val A -> exp S B) -> exp val (A => B).
app :
   {S1:stlc_sort} {A:tp} {B:tp} {S2:stlc_sort}
      exp S1 (A => B) -> exp S2 A -> exp non-val B.
eval : {S:stlc_sort} {A:tp} exp S A -> exp val A -> type.
ev-lam :
   {X1:tp} {X2:tp} {X3:stlc_sort} {E:exp val X1 -> exp X3 X2}
      eval (lam ([x:exp val X1] E x)) (lam ([x:exp val X1] E x)).
ev-app :
   {X1:stlc_sort} {X2:tp} {X3:tp} {E1':exp val X3 -> exp X1 X2} {V2:exp val X3}
      {V:exp val X2} {X4:stlc_sort} {E2:exp X4 X3} {X5:stlc_sort}
      {E1:exp X5 (X3 => X2)}
      eval (E1' V2) V -> eval E2 V2 -> eval E1 (lam ([x:exp val X3] E1' x))
         -> eval (app E1 E2) V.
[Closing file /home/www/twelf/hcode/3e16e789fef6385b35884575bc350848]
%% OK %%