DEFINITION getl_ctail_clen()
TYPE =
       ∀b:B
         .∀t:T
           .∀c:C
             .ex
               nat
               λn:nat
                 .getl
                   clen c
                   CTail (Bind b) t c
                   CHead (CSort n) (Bind b) t
BODY =
        assume b: B
        assume t: T
        assume c: C
          we proceed by induction on c to prove 
             ex
               nat
               λn:nat
                 .getl
                   clen c
                   CTail (Bind b) t c
                   CHead (CSort n) (Bind b) t
             case CSort : n:nat ⇒
                the thesis becomes 
                ex
                  nat
                  λn:nat
                    .getl
                      clen (CSort n)
                      CTail (Bind b) t (CSort n)
                      CHead (CSort n) (Bind b) t
                   by (getl_refl . . .)
                   we proved 
                      getl
                        O
                        CHead (CSort n) (Bind b) t
                        CHead (CSort n) (Bind b) t
                   by (ex_intro . . . previous)
                   we proved 
                      ex
                        nat
                        λn0:nat
                          .getl
                            O
                            CHead (CSort n) (Bind b) t
                            CHead (CSort n0) (Bind b) t

                      ex
                        nat
                        λn:nat
                          .getl
                            clen (CSort n)
                            CTail (Bind b) t (CSort n)
                            CHead (CSort n) (Bind b) t
             case CHead : c0:C k:K t0:T ⇒
                the thesis becomes 
                ex
                  nat
                  λn:nat
                    .getl
                      clen (CHead c0 k t0)
                      CTail (Bind b) t (CHead c0 k t0)
                      CHead (CSort n) (Bind b) t
                (H) by induction hypothesis we know 
                   ex
                     nat
                     λn:nat
                       .getl
                         clen c0
                         CTail (Bind b) t c0
                         CHead (CSort n) (Bind b) t
                   (H0) consider H
                   we proceed by induction on H0 to prove 
                      ex
                        nat
                        λn:nat
                          .getl
                            s k (clen c0)
                            CHead (CTail (Bind b) t c0) k t0
                            CHead (CSort n) (Bind b) t
                      case ex_intro : x:nat H1:getl (clen c0) (CTail (Bind b) t c0) (CHead (CSort x) (Bind b) t) ⇒
                         the thesis becomes 
                         ex
                           nat
                           λn:nat
                             .getl
                               s k (clen c0)
                               CHead (CTail (Bind b) t c0) k t0
                               CHead (CSort n) (Bind b) t
                            we proceed by induction on k to prove 
                               ex
                                 nat
                                 λn:nat
                                   .getl
                                     s k (clen c0)
                                     CHead (CTail (Bind b) t c0) k t0
                                     CHead (CSort n) (Bind b) t
                               case Bind : b0:B ⇒
                                  the thesis becomes 
                                  ex
                                    nat
                                    λn:nat
                                      .getl
                                        s (Bind b0) (clen c0)
                                        CHead (CTail (Bind b) t c0) (Bind b0) t0
                                        CHead (CSort n) (Bind b) t
                                     consider H1
                                     we proved 
                                        getl
                                          clen c0
                                          CTail (Bind b) t c0
                                          CHead (CSort x) (Bind b) t
                                     that is equivalent to 
                                        getl
                                          r (Bind b0) (clen c0)
                                          CTail (Bind b) t c0
                                          CHead (CSort x) (Bind b) t
                                     by (getl_head . . . . previous .)
                                     we proved 
                                        getl
                                          S (clen c0)
                                          CHead (CTail (Bind b) t c0) (Bind b0) t0
                                          CHead (CSort x) (Bind b) t
                                     by (ex_intro . . . previous)
                                     we proved 
                                        ex
                                          nat
                                          λn:nat
                                            .getl
                                              S (clen c0)
                                              CHead (CTail (Bind b) t c0) (Bind b0) t0
                                              CHead (CSort n) (Bind b) t

                                        ex
                                          nat
                                          λn:nat
                                            .getl
                                              s (Bind b0) (clen c0)
                                              CHead (CTail (Bind b) t c0) (Bind b0) t0
                                              CHead (CSort n) (Bind b) t
                               case Flat : f:F ⇒
                                  the thesis becomes 
                                  ex
                                    nat
                                    λn:nat
                                      .getl
                                        s (Flat f) (clen c0)
                                        CHead (CTail (Bind b) t c0) (Flat f) t0
                                        CHead (CSort n) (Bind b) t
                                     by (getl_flat . . . H1 . .)
                                     we proved 
                                        getl
                                          clen c0
                                          CHead (CTail (Bind b) t c0) (Flat f) t0
                                          CHead (CSort x) (Bind b) t
                                     by (ex_intro . . . previous)
                                     we proved 
                                        ex
                                          nat
                                          λn:nat
                                            .getl
                                              clen c0
                                              CHead (CTail (Bind b) t c0) (Flat f) t0
                                              CHead (CSort n) (Bind b) t

                                        ex
                                          nat
                                          λn:nat
                                            .getl
                                              s (Flat f) (clen c0)
                                              CHead (CTail (Bind b) t c0) (Flat f) t0
                                              CHead (CSort n) (Bind b) t

                               ex
                                 nat
                                 λn:nat
                                   .getl
                                     s k (clen c0)
                                     CHead (CTail (Bind b) t c0) k t0
                                     CHead (CSort n) (Bind b) t
                   we proved 
                      ex
                        nat
                        λn:nat
                          .getl
                            s k (clen c0)
                            CHead (CTail (Bind b) t c0) k t0
                            CHead (CSort n) (Bind b) t

                      ex
                        nat
                        λn:nat
                          .getl
                            clen (CHead c0 k t0)
                            CTail (Bind b) t (CHead c0 k t0)
                            CHead (CSort n) (Bind b) t
          we proved 
             ex
               nat
               λn:nat
                 .getl
                   clen c
                   CTail (Bind b) t c
                   CHead (CSort n) (Bind b) t
       we proved 
          ∀b:B
            .∀t:T
              .∀c:C
                .ex
                  nat
                  λn:nat
                    .getl
                      clen c
                      CTail (Bind b) t c
                      CHead (CSort n) (Bind b) t