Twelf 1.5R3, Aug 30, 2005 (%trustme)
%% OK %%
[Opening file /home/www/twelf/hcode/eb0a13534276e5207e1d788f3bd0338c]
t : type.
cat : type = t -> t -> t -> t -> t -> t -> t -> t.
k : t -> t -> t -> t -> t -> t -> t -> t
   = [k:t] [a:t] [p:t] [m:t] [r:t] [m+r:t] [u:t] k.
a : t -> t -> t -> t -> t -> t -> t -> t
   = [k1:t] [a:t] [p:t] [m:t] [r:t] [m+r:t] [u:t] a.
p : t -> t -> t -> t -> t -> t -> t -> t
   = [k1:t] [a1:t] [p:t] [m:t] [r:t] [m+r:t] [u:t] p.
m : t -> t -> t -> t -> t -> t -> t -> t
   = [k1:t] [a1:t] [p1:t] [m:t] [r:t] [m+r:t] [u:t] m.
r : t -> t -> t -> t -> t -> t -> t -> t
   = [k1:t] [a1:t] [p1:t] [m1:t] [r:t] [m+r:t] [u:t] r.
m+r : t -> t -> t -> t -> t -> t -> t -> t
   = [k1:t] [a1:t] [p1:t] [m1:t] [r1:t] [m+r:t] [u:t] m+r.
u : t -> t -> t -> t -> t -> t -> t -> t
   = [k1:t] [a1:t] [p1:t] [m1:t] [r1:t] [m+r1:t] [u:t] u.
tm : (t -> t -> t -> t -> t -> t -> t -> t) -> type.
typ : tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x).
pi_k :
   tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)
      -> (tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
             -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x))
      -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x).
coer_pa :
   tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x2)
      -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1).
pi_a :
   tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)
      -> (tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
             -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1))
      -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1).
app_p :
   tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x2)
      -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)
      -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x2).
coer_rm :
   tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
      -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3).
lam_m :
   (tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
       -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3))
      -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3).
app_r :
   tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
      -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)
      -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4).
canon :
   tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)
      -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x5).
atom :
   tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
      -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x5).
* : tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x6).
class :
   (t -> t -> t -> t -> t -> t -> t -> t) -> t -> t -> t -> t -> t -> t -> t
      -> t
   = [X:t -> t -> t -> t -> t -> t -> t -> t] [k1:t] [a1:t] [p1:t] [m1:t] [r1:t]
        [m+r1:t] [u1:t] X u1 u1 k1 a1 a1 a1 u1.
subst :
   (t -> t -> t -> t -> t -> t -> t -> t) -> t -> t -> t -> t -> t -> t -> t
      -> t
   = [X:t -> t -> t -> t -> t -> t -> t -> t] [k1:t] [a1:t] [p1:t] [m1:t] [r1:t]
        [m+r1:t] [u1:t] X k1 a1 p1 m1 m+r1 m+r1 u1.
classj :
   {X:t -> t -> t -> t -> t -> t -> t -> t}
      tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] X x x1 x2 x3 x4 x5 x6)
         -> tm
               ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t]
                   X x6 x6 x x1 x1 x1 x6) -> type.
substj :
   {X:t -> t -> t -> t -> t -> t -> t -> t}
      (tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
          -> tm
                ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t]
                    X x x1 x2 x3 x4 x5 x6))
         -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)
         -> tm
               ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t]
                   X x x1 x2 x3 x5 x5 x6) -> type.
canon_kind_type : classj typ *.
canon_kind_pi :
   {A2:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      {K:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x)}
      ({y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
          classj y A2 -> classj (K y) *)
         -> classj A2 *
         -> classj
               (pi_k A2
                   ([y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                       K y))
               *.
canon_fam_pi :
   {A2:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      {A:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      ({y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
          classj y A2 -> classj (A y) *)
         -> classj A2 *
         -> classj
               (pi_a A2
                   ([y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                       A y))
               *.
canon_fam_atom :
   {P:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x2)}
      classj P typ -> classj (coer_pa P) *.
atom_fam_app :
   {K1:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
          -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x)}
      {M2:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {K:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x)}
      {A2:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      {P1:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x2)}
      substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] K1 x)
         M2 K
         -> classj M2 A2
         -> classj P1
               (pi_k A2
                   ([y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                       K1 y))
         -> classj (app_p P1 M2) K.
canon_term_lam :
   {A2:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      {M:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {A:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      ({y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
          classj y A2 -> classj (M y) (A y))
         -> classj
               (lam_m
                   ([y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                       M y))
               (pi_a A2
                   ([y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                       A y)).
canon_term_atom :
   {R:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
      {P:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x2)}
      classj R (coer_pa P) -> classj (coer_rm R) (coer_pa P).
atom_term_app :
   {A1:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
          -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      {M2:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {A:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      {A2:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      {R1:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
      substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] A1 x)
         M2 A
         -> classj M2 A2
         -> classj R1
               (pi_a A2
                   ([y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                       A1 y))
         -> classj (app_r R1 M2) A.
canon_atom_can :
   {M:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {A:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      classj M A -> classj (canon M) A.
canon_atom_atom :
   {R:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
      {A:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      classj R A -> classj (atom R) A.
unit_unit : classj * *.
subst_k_type :
   {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] typ)
         M0 typ.
subst_k_pi :
   {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {K:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x)}
      {K':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
             -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x)}
      {A:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      {A':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      ({y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
          substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] y)
             M0 (atom y)
             -> substj
                   ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                       K x y)
                   M0 (K' y))
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] A x)
               M0 A'
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                   pi_k (A x)
                      ([y:tm
                             ([x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] [x7:t]
                                 x5)]
                          K x y))
               M0
               (pi_k A'
                   ([y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                       K' y)).
subst_a_p :
   {P:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
         -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x2)}
      {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {P':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x2)}
      substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] P x)
         M0 P'
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                   coer_pa (P x)) M0
               (coer_pa P').
subst_a_pi :
   {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {A:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      {A':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
             -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      {A2:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
             -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      {A2':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      ({y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
          substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] y)
             M0 (atom y)
             -> substj
                   ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                       A x y)
                   M0 (A' y))
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] 
A2 x)
               M0 A2'
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                   pi_a (A2 x)
                      ([y:tm
                             ([x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] [x7:t]
                                 x5)]
                          A x y))
               M0
               (pi_a A2'
                   ([y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                       A' y)).
subst_p_app :
   {M:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
         -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {M':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {P:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x2)}
      {P':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x2)}
      substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] M x)
         M0 M'
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] P x)
               M0 P'
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                   app_p (P x) (M x)) M0
               (app_p P' M').
subst_m_lam :
   {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {M:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {M':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
             -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      ({y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
          substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] y)
             M0 (atom y)
             -> substj
                   ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                       M x y)
                   M0 (M' y))
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                   lam_m
                      ([y:tm
                             ([x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] [x7:t]
                                 x5)]
                          M x y))
               M0
               (lam_m
                   ([y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                       M' y)).
subst_m_rh :
   {R:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
         -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
      {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {M':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] R x)
         M0 (canon M')
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                   coer_rm (R x)) M0
               M'.
subst_m_r :
   {R:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
         -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
      {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {R':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
      substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] R x)
         M0 (atom R')
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                   coer_rm (R x)) M0
               (coer_rm R').
subst_rh_var :
   {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] x) M0
         (canon M0).
subst_rh_app :
   {M':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
          -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {M2':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {M'':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {M2:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
             -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {R1:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
             -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
      substj ([y:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] M' y)
         M2' M''
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] 
M2 x)
               M0 M2'
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] 
R1 x)
               M0
               (canon
                   (lam_m
                       ([y:tm
                              ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t]
                                  x4)]
                           M' y)))
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                   app_r (R1 x) (M2 x)) M0
               (canon M'').
subst_r_app :
   {M2:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
          -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {M2':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {R1:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
             -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
      {R1':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
      substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] M2 x)
         M0 M2'
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] 
R1 x)
               M0 (atom R1')
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                   app_r (R1 x) (M2 x)) M0
               (atom (app_r R1' M2')).
subst_m+r_canon :
   {M:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
         -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {M':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] M x)
         M0 M'
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                   canon (M x)) M0
               (canon M').
subst_m+r_atom :
   {P:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
         -> tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
      {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {P':tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
      substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] P x)
         M0 (atom P')
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                   atom (P x)) M0
               (atom P').
subst_unit_unit :
   {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      substj ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] *) M0
         *.
sub_thm :
   {X:t -> t -> t -> t -> t -> t -> t -> t}
      {M0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x3)}
      {A0:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x1)}
      {C:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm
                  ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t]
                      X x6 x6 x x1 x1 x1 x6)}
      {C':tm
             ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t]
                 X x6 x6 x x1 x1 x1 x6)}
      {T:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)
            -> tm
                  ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t]
                      X x x1 x2 x3 x4 x5 x6)}
      classj M0 A0
         -> ({x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)}
                classj x A0 -> classj (T x) (C x))
         -> substj
               ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)] C x)
               M0 C'
         -> ({T':tm
                    ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t]
                        X x x1 x2 x3 x5 x5 x6)}
                substj
                   ([x:tm ([x:t] [x1:t] [x2:t] [x3:t] [x4:t] [x5:t] [x6:t] x4)]
                       T x)
                   M0 T'
                   -> classj T' C' -> type).
[Closing file /home/www/twelf/hcode/eb0a13534276e5207e1d788f3bd0338c]
%% OK %%