Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/bf5353c352d546381d224b2aa176527e]
tp : type.
tp/unit : tp.
tp/arrow : tp -> tp -> tp.
exp : type.
exp/unit : exp.
exp/lam : tp -> (exp -> exp) -> exp.
exp/app : exp -> exp -> exp.
of : exp -> tp -> type.
of/unit : of exp/unit tp/unit.
of/lam :
   {T:tp} {E:exp -> exp} {T':tp}
      ({x:exp} of x T -> of (E x) T')
         -> of (exp/lam T ([x:exp] E x)) (tp/arrow T T').
of/app :
   {E1:exp} {T:tp} {T':tp} {E2:exp}
      of E1 (tp/arrow T T') -> of E2 T -> of (exp/app E1 E2) T'.
subst :
   {E1:exp} {T:tp} {E2:exp -> exp} {T':tp}
      of E1 T -> ({x:exp} of x T -> of (E2 x) T') -> of (E2 E1) T' -> type.
%mode +{E1:exp} +{T:tp} +{E2:exp -> exp} +{T':tp} +{D1:of E1 T}
   +{D2:{x:exp} of x T -> of (E2 x) T'} -{D3:of (E2 E1) T'} (subst D1 D2 D3).
- :
   {E1:exp} {X1:tp} {X2:exp -> exp} {X3:tp} {D1:of E1 X1}
      {D2:{x:exp} of x X1 -> of (X2 x) X3}
      subst D1 ([x:exp] [dx:of x X1] D2 x dx) (D2 E1 D1).
%block of-block : some {T:tp} block {x:exp} {dx:of x T}.
%worlds (of-block) (subst _ _ _).
%total {} (subst _ _ _).
[Closing file /home/www/twelfwiki/code/bf5353c352d546381d224b2aa176527e]
%% OK %%