DEFINITION node_inh()
TYPE =
       ∀g:G.∀n:nat.∀k:nat.(ex_2 C T λc:C.λt:T.arity g c t (ASort k n))
BODY =
        assume g: G
        assume n: nat
        assume k: nat
          we proceed by induction on k to prove ex_2 C T λc:C.λt:T.arity g c t (ASort k n)
             case O : ⇒
                the thesis becomes ex_2 C T λc:C.λt:T.arity g c t (ASort O n)
                   by (arity_sort . . .)
                   we proved arity g (CSort O) (TSort n) (ASort O n)
                   by (ex_2_intro . . . . . previous)
ex_2 C T λc:C.λt:T.arity g c t (ASort O n)
             case S : n0:nat ⇒
                the thesis becomes ex_2 C T λc:C.λt:T.arity g c t (ASort (S n0) n)
                (H) by induction hypothesis we know ex_2 C T λc:C.λt:T.arity g c t (ASort n0 n)
                   (H0) consider H
                   we proceed by induction on H0 to prove ex_2 C T λc:C.λt:T.arity g c t (ASort (S n0) n)
                      case ex_2_intro : x0:C x1:T H1:arity g x0 x1 (ASort n0 n) ⇒
                         the thesis becomes ex_2 C T λc:C.λt:T.arity g c t (ASort (S n0) n)
                            (h1) 
                               by (getl_refl . . .)
getl O (CHead x0 (Bind Abst) x1) (CHead x0 (Bind Abst) x1)
                            end of h1
                            (h2) 
                               consider H1
                               we proved arity g x0 x1 (ASort n0 n)
arity g x0 x1 (asucc g (ASort (S n0) n))
                            end of h2
                            by (arity_abst . . . . . h1 . h2)
                            we proved arity g (CHead x0 (Bind Abst) x1) (TLRef O) (ASort (S n0) n)
                            by (ex_2_intro . . . . . previous)
ex_2 C T λc:C.λt:T.arity g c t (ASort (S n0) n)
ex_2 C T λc:C.λt:T.arity g c t (ASort (S n0) n)
          we proved ex_2 C T λc:C.λt:T.arity g c t (ASort k n)
       we proved ∀g:G.∀n:nat.∀k:nat.(ex_2 C T λc:C.λt:T.arity g c t (ASort k n))