DEFINITION getl_gen_tail()
TYPE =
       k:K
         .b:B
           .u1:T
             .u2:T
               .c2:C
                 .c1:C
                   .i:nat
                     .getl i (CTail k u1 c1) (CHead c2 (Bind b) u2)
                       (or
                            ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl i c1 (CHead e (Bind b) u2)
                            ex4
                              nat
                              λ:nat.eq nat i (clen c1)
                              λ:nat.eq K k (Bind b)
                              λ:nat.eq T u1 u2
                              λn:nat.eq C c2 (CSort n))
BODY =
        assume kK
        assume bB
        assume u1T
        assume u2T
        assume c2C
        assume c1C
          we proceed by induction on c1 to prove 
             i:nat
               .getl i (CTail k u1 c1) (CHead c2 (Bind b) u2)
                 (or
                      ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl i c1 (CHead e (Bind b) u2)
                      ex4
                        nat
                        λ:nat.eq nat i (clen c1)
                        λ:nat.eq K k (Bind b)
                        λ:nat.eq T u1 u2
                        λn:nat.eq C c2 (CSort n))
             case CSort : n:nat 
                the thesis becomes 
                i:nat
                  .getl i (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
                    (or
                         ex2
                           C
                           λe:C.eq C c2 (CTail k u1 e)
                           λe:C.getl i (CSort n) (CHead e (Bind b) u2)
                         ex4
                           nat
                           λ:nat.eq nat i (clen (CSort n))
                           λ:nat.eq K k (Bind b)
                           λ:nat.eq T u1 u2
                           λn1:nat.eq C c2 (CSort n1))
                   assume inat
                      we proceed by induction on i to prove 
                         getl i (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
                           (or
                                ex2
                                  C
                                  λe:C.eq C c2 (CTail k u1 e)
                                  λe:C.getl i (CSort n) (CHead e (Bind b) u2)
                                ex4
                                  nat
                                  λ:nat.eq nat i (clen (CSort n))
                                  λ:nat.eq K k (Bind b)
                                  λ:nat.eq T u1 u2
                                  λn1:nat.eq C c2 (CSort n1))
                         case O : 
                            the thesis becomes 
                            getl O (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
                              (or
                                   ex2
                                     C
                                     λe:C.eq C c2 (CTail k u1 e)
                                     λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                   ex4
                                     nat
                                     λ:nat.eq nat O (clen (CSort n))
                                     λ:nat.eq K k (Bind b)
                                     λ:nat.eq T u1 u2
                                     λn1:nat.eq C c2 (CSort n1))
                               we must prove 
                                     getl O (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
                                       (or
                                            ex2
                                              C
                                              λe:C.eq C c2 (CTail k u1 e)
                                              λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                            ex4
                                              nat
                                              λ:nat.eq nat O (clen (CSort n))
                                              λ:nat.eq K k (Bind b)
                                              λ:nat.eq T u1 u2
                                              λn1:nat.eq C c2 (CSort n1))
                               or equivalently 
                                     getl O (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
                                       (or
                                            ex2
                                              C
                                              λe:C.eq C c2 (CTail k u1 e)
                                              λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                            ex4
                                              nat
                                              λ:nat.eq nat O (clen (CSort n))
                                              λ:nat.eq K k (Bind b)
                                              λ:nat.eq T u1 u2
                                              λn1:nat.eq C c2 (CSort n1))
                               suppose Hgetl O (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
                                  by (getl_gen_O . . H)
                                  we proved clear (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
                                     assume b0B
                                     suppose H0clear (CHead (CSort n) (Bind b0) u1) (CHead c2 (Bind b) u2)
                                        (H1
                                           by (clear_gen_bind . . . . H0)
                                           we proved eq C (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind b0) u1)
                                           by (f_equal . . . . . previous)
                                           we proved 
                                              eq
                                                C
                                                <λ:C.C> CASE CHead c2 (Bind b) u2 OF CSort c2 | CHead c  c
                                                <λ:C.C> CASE CHead (CSort n) (Bind b0) u1 OF CSort c2 | CHead c  c

                                              eq
                                                C
                                                λe:C.<λ:C.C> CASE e OF CSort c2 | CHead c  c (CHead c2 (Bind b) u2)
                                                λe:C.<λ:C.C> CASE e OF CSort c2 | CHead c  c
                                                  CHead (CSort n) (Bind b0) u1
                                        end of H1
                                        (h1
                                           (H2
                                              by (clear_gen_bind . . . . H0)
                                              we proved eq C (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind b0) u1)
                                              by (f_equal . . . . . previous)
                                              we proved 
                                                 eq
                                                   B
                                                   <λ:C.B>
                                                     CASE CHead c2 (Bind b) u2 OF
                                                       CSort b
                                                     | CHead  k0 <λ:K.B> CASE k0 OF Bind b1b1 | Flat b
                                                   <λ:C.B>
                                                     CASE CHead (CSort n) (Bind b0) u1 OF
                                                       CSort b
                                                     | CHead  k0 <λ:K.B> CASE k0 OF Bind b1b1 | Flat b

                                                 eq
                                                   B
                                                   λe:C.<λ:C.B> CASE e OF CSort b | CHead  k0 <λ:K.B> CASE k0 OF Bind b1b1 | Flat b
                                                     CHead c2 (Bind b) u2
                                                   λe:C.<λ:C.B> CASE e OF CSort b | CHead  k0 <λ:K.B> CASE k0 OF Bind b1b1 | Flat b
                                                     CHead (CSort n) (Bind b0) u1
                                           end of H2
                                           (h1
                                              (H3
                                                 by (clear_gen_bind . . . . H0)
                                                 we proved eq C (CHead c2 (Bind b) u2) (CHead (CSort n) (Bind b0) u1)
                                                 by (f_equal . . . . . previous)
                                                 we proved 
                                                    eq
                                                      T
                                                      <λ:C.T> CASE CHead c2 (Bind b) u2 OF CSort u2 | CHead   tt
                                                      <λ:C.T> CASE CHead (CSort n) (Bind b0) u1 OF CSort u2 | CHead   tt

                                                    eq
                                                      T
                                                      λe:C.<λ:C.T> CASE e OF CSort u2 | CHead   tt (CHead c2 (Bind b) u2)
                                                      λe:C.<λ:C.T> CASE e OF CSort u2 | CHead   tt
                                                        CHead (CSort n) (Bind b0) u1
                                              end of H3
                                               suppose H4eq B b b0
                                               suppose H5eq C c2 (CSort n)
                                                 (h1
                                                    (h1
                                                       by (refl_equal . .)
eq nat O O
                                                    end of h1
                                                    (h2
                                                       by (refl_equal . .)
eq K (Bind b0) (Bind b0)
                                                    end of h2
                                                    (h3
                                                       by (refl_equal . .)
eq T u1 u1
                                                    end of h3
                                                    (h4
                                                       by (refl_equal . .)
eq C (CSort n) (CSort n)
                                                    end of h4
                                                    by (ex4_intro . . . . . . h1 h2 h3 h4)
                                                    we proved 
                                                       ex4
                                                         nat
                                                         λ:nat.eq nat O O
                                                         λ:nat.eq K (Bind b0) (Bind b0)
                                                         λ:nat.eq T u1 u1
                                                         λn0:nat.eq C (CSort n) (CSort n0)
                                                    by (or_intror . . previous)
                                                    we proved 
                                                       or
                                                         ex2
                                                           C
                                                           λe:C.eq C (CSort n) (CTail (Bind b0) u1 e)
                                                           λe:C.getl O (CSort n) (CHead e (Bind b0) u1)
                                                         ex4
                                                           nat
                                                           λ:nat.eq nat O O
                                                           λ:nat.eq K (Bind b0) (Bind b0)
                                                           λ:nat.eq T u1 u1
                                                           λn0:nat.eq C (CSort n) (CSort n0)
                                                    by (eq_ind_r . . . previous . H4)

                                                       or
                                                         ex2
                                                           C
                                                           λe:C.eq C (CSort n) (CTail (Bind b0) u1 e)
                                                           λe:C.getl O (CSort n) (CHead e (Bind b) u1)
                                                         ex4
                                                           nat
                                                           λ:nat.eq nat O O
                                                           λ:nat.eq K (Bind b0) (Bind b)
                                                           λ:nat.eq T u1 u1
                                                           λn0:nat.eq C (CSort n) (CSort n0)
                                                 end of h1
                                                 (h2
                                                    consider H3
                                                    we proved 
                                                       eq
                                                         T
                                                         <λ:C.T> CASE CHead c2 (Bind b) u2 OF CSort u2 | CHead   tt
                                                         <λ:C.T> CASE CHead (CSort n) (Bind b0) u1 OF CSort u2 | CHead   tt
eq T u2 u1
                                                 end of h2
                                                 by (eq_ind_r . . . h1 . h2)
                                                 we proved 
                                                    or
                                                      ex2
                                                        C
                                                        λe:C.eq C (CSort n) (CTail (Bind b0) u1 e)
                                                        λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                                      ex4
                                                        nat
                                                        λ:nat.eq nat O O
                                                        λ:nat.eq K (Bind b0) (Bind b)
                                                        λ:nat.eq T u1 u2
                                                        λn0:nat.eq C (CSort n) (CSort n0)
                                                 by (eq_ind_r . . . previous . H5)
                                                 we proved 
                                                    or
                                                      ex2
                                                        C
                                                        λe:C.eq C c2 (CTail (Bind b0) u1 e)
                                                        λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                                      ex4
                                                        nat
                                                        λ:nat.eq nat O O
                                                        λ:nat.eq K (Bind b0) (Bind b)
                                                        λ:nat.eq T u1 u2
                                                        λn0:nat.eq C c2 (CSort n0)

                                                 eq B b b0
                                                   (eq C c2 (CSort n)
                                                        (or
                                                             ex2
                                                               C
                                                               λe:C.eq C c2 (CTail (Bind b0) u1 e)
                                                               λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                                             ex4
                                                               nat
                                                               λ:nat.eq nat O O
                                                               λ:nat.eq K (Bind b0) (Bind b)
                                                               λ:nat.eq T u1 u2
                                                               λn0:nat.eq C c2 (CSort n0)))
                                           end of h1
                                           (h2
                                              consider H2
                                              we proved 
                                                 eq
                                                   B
                                                   <λ:C.B>
                                                     CASE CHead c2 (Bind b) u2 OF
                                                       CSort b
                                                     | CHead  k0 <λ:K.B> CASE k0 OF Bind b1b1 | Flat b
                                                   <λ:C.B>
                                                     CASE CHead (CSort n) (Bind b0) u1 OF
                                                       CSort b
                                                     | CHead  k0 <λ:K.B> CASE k0 OF Bind b1b1 | Flat b
eq B b b0
                                           end of h2
                                           by (h1 h2)

                                              eq C c2 (CSort n)
                                                (or
                                                     ex2
                                                       C
                                                       λe:C.eq C c2 (CTail (Bind b0) u1 e)
                                                       λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                                     ex4
                                                       nat
                                                       λ:nat.eq nat O O
                                                       λ:nat.eq K (Bind b0) (Bind b)
                                                       λ:nat.eq T u1 u2
                                                       λn0:nat.eq C c2 (CSort n0))
                                        end of h1
                                        (h2
                                           consider H1
                                           we proved 
                                              eq
                                                C
                                                <λ:C.C> CASE CHead c2 (Bind b) u2 OF CSort c2 | CHead c  c
                                                <λ:C.C> CASE CHead (CSort n) (Bind b0) u1 OF CSort c2 | CHead c  c
eq C c2 (CSort n)
                                        end of h2
                                        by (h1 h2)
                                        we proved 
                                           or
                                             ex2
                                               C
                                               λe:C.eq C c2 (CTail (Bind b0) u1 e)
                                               λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                             ex4
                                               nat
                                               λ:nat.eq nat O O
                                               λ:nat.eq K (Bind b0) (Bind b)
                                               λ:nat.eq T u1 u2
                                               λn0:nat.eq C c2 (CSort n0)

                                        H0:clear (CHead (CSort n) (Bind b0) u1) (CHead c2 (Bind b) u2)
                                          .or
                                            ex2
                                              C
                                              λe:C.eq C c2 (CTail (Bind b0) u1 e)
                                              λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                            ex4
                                              nat
                                              λ:nat.eq nat O O
                                              λ:nat.eq K (Bind b0) (Bind b)
                                              λ:nat.eq T u1 u2
                                              λn0:nat.eq C c2 (CSort n0)
                                     assume fF
                                     suppose H0clear (CHead (CSort n) (Flat f) u1) (CHead c2 (Bind b) u2)
                                        by (clear_gen_flat . . . . H0)
                                        we proved clear (CSort n) (CHead c2 (Bind b) u2)
                                        by (clear_gen_sort . . previous .)
                                        we proved 
                                           or
                                             ex2
                                               C
                                               λe:C.eq C c2 (CTail (Flat f) u1 e)
                                               λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                             ex4
                                               nat
                                               λ:nat.eq nat O O
                                               λ:nat.eq K (Flat f) (Bind b)
                                               λ:nat.eq T u1 u2
                                               λn0:nat.eq C c2 (CSort n0)

                                        H0:clear (CHead (CSort n) (Flat f) u1) (CHead c2 (Bind b) u2)
                                          .or
                                            ex2
                                              C
                                              λe:C.eq C c2 (CTail (Flat f) u1 e)
                                              λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                            ex4
                                              nat
                                              λ:nat.eq nat O O
                                              λ:nat.eq K (Flat f) (Bind b)
                                              λ:nat.eq T u1 u2
                                              λn0:nat.eq C c2 (CSort n0)
                                  by (previous . previous)
                                  we proved 
                                     or
                                       ex2
                                         C
                                         λe:C.eq C c2 (CTail k u1 e)
                                         λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                       ex4
                                         nat
                                         λ:nat.eq nat O O
                                         λ:nat.eq K k (Bind b)
                                         λ:nat.eq T u1 u2
                                         λn0:nat.eq C c2 (CSort n0)
                                  that is equivalent to 
                                     or
                                       ex2
                                         C
                                         λe:C.eq C c2 (CTail k u1 e)
                                         λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                       ex4
                                         nat
                                         λ:nat.eq nat O (clen (CSort n))
                                         λ:nat.eq K k (Bind b)
                                         λ:nat.eq T u1 u2
                                         λn1:nat.eq C c2 (CSort n1)
                               we proved 
                                  getl O (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
                                    (or
                                         ex2
                                           C
                                           λe:C.eq C c2 (CTail k u1 e)
                                           λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                         ex4
                                           nat
                                           λ:nat.eq nat O (clen (CSort n))
                                           λ:nat.eq K k (Bind b)
                                           λ:nat.eq T u1 u2
                                           λn1:nat.eq C c2 (CSort n1))

                                  getl O (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
                                    (or
                                         ex2
                                           C
                                           λe:C.eq C c2 (CTail k u1 e)
                                           λe:C.getl O (CSort n) (CHead e (Bind b) u2)
                                         ex4
                                           nat
                                           λ:nat.eq nat O (clen (CSort n))
                                           λ:nat.eq K k (Bind b)
                                           λ:nat.eq T u1 u2
                                           λn1:nat.eq C c2 (CSort n1))
                         case S : n0:nat 
                            the thesis becomes 
                            getl (S n0) (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
                              (or
                                   ex2
                                     C
                                     λe:C.eq C c2 (CTail k u1 e)
                                     λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
                                   ex4
                                     nat
                                     λ:nat.eq nat (S n0) (clen (CSort n))
                                     λ:nat.eq K k (Bind b)
                                     λ:nat.eq T u1 u2
                                     λn1:nat.eq C c2 (CSort n1))
                            () by induction hypothesis we know 
                               getl n0 (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
                                 (or
                                      ex2
                                        C
                                        λe:C.eq C c2 (CTail k u1 e)
                                        λe:C.getl n0 (CSort n) (CHead e (Bind b) u2)
                                      ex4
                                        nat
                                        λ:nat.eq nat n0 O
                                        λ:nat.eq K k (Bind b)
                                        λ:nat.eq T u1 u2
                                        λn1:nat.eq C c2 (CSort n1))
                               we must prove 
                                     getl (S n0) (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
                                       (or
                                            ex2
                                              C
                                              λe:C.eq C c2 (CTail k u1 e)
                                              λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
                                            ex4
                                              nat
                                              λ:nat.eq nat (S n0) (clen (CSort n))
                                              λ:nat.eq K k (Bind b)
                                              λ:nat.eq T u1 u2
                                              λn1:nat.eq C c2 (CSort n1))
                               or equivalently 
                                     getl (S n0) (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
                                       (or
                                            ex2
                                              C
                                              λe:C.eq C c2 (CTail k u1 e)
                                              λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
                                            ex4
                                              nat
                                              λ:nat.eq nat (S n0) (clen (CSort n))
                                              λ:nat.eq K k (Bind b)
                                              λ:nat.eq T u1 u2
                                              λn1:nat.eq C c2 (CSort n1))
                               suppose H0getl (S n0) (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
                                  by (getl_gen_S . . . . . H0)
                                  we proved getl (r k n0) (CSort n) (CHead c2 (Bind b) u2)
                                  by (getl_gen_sort . . . previous .)
                                  we proved 
                                     or
                                       ex2
                                         C
                                         λe:C.eq C c2 (CTail k u1 e)
                                         λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
                                       ex4
                                         nat
                                         λ:nat.eq nat (S n0) O
                                         λ:nat.eq K k (Bind b)
                                         λ:nat.eq T u1 u2
                                         λn1:nat.eq C c2 (CSort n1)
                                  that is equivalent to 
                                     or
                                       ex2
                                         C
                                         λe:C.eq C c2 (CTail k u1 e)
                                         λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
                                       ex4
                                         nat
                                         λ:nat.eq nat (S n0) (clen (CSort n))
                                         λ:nat.eq K k (Bind b)
                                         λ:nat.eq T u1 u2
                                         λn1:nat.eq C c2 (CSort n1)
                               we proved 
                                  getl (S n0) (CHead (CSort n) k u1) (CHead c2 (Bind b) u2)
                                    (or
                                         ex2
                                           C
                                           λe:C.eq C c2 (CTail k u1 e)
                                           λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
                                         ex4
                                           nat
                                           λ:nat.eq nat (S n0) (clen (CSort n))
                                           λ:nat.eq K k (Bind b)
                                           λ:nat.eq T u1 u2
                                           λn1:nat.eq C c2 (CSort n1))

                                  getl (S n0) (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
                                    (or
                                         ex2
                                           C
                                           λe:C.eq C c2 (CTail k u1 e)
                                           λe:C.getl (S n0) (CSort n) (CHead e (Bind b) u2)
                                         ex4
                                           nat
                                           λ:nat.eq nat (S n0) (clen (CSort n))
                                           λ:nat.eq K k (Bind b)
                                           λ:nat.eq T u1 u2
                                           λn1:nat.eq C c2 (CSort n1))
                      we proved 
                         getl i (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
                           (or
                                ex2
                                  C
                                  λe:C.eq C c2 (CTail k u1 e)
                                  λe:C.getl i (CSort n) (CHead e (Bind b) u2)
                                ex4
                                  nat
                                  λ:nat.eq nat i (clen (CSort n))
                                  λ:nat.eq K k (Bind b)
                                  λ:nat.eq T u1 u2
                                  λn1:nat.eq C c2 (CSort n1))

                      i:nat
                        .getl i (CTail k u1 (CSort n)) (CHead c2 (Bind b) u2)
                          (or
                               ex2
                                 C
                                 λe:C.eq C c2 (CTail k u1 e)
                                 λe:C.getl i (CSort n) (CHead e (Bind b) u2)
                               ex4
                                 nat
                                 λ:nat.eq nat i (clen (CSort n))
                                 λ:nat.eq K k (Bind b)
                                 λ:nat.eq T u1 u2
                                 λn1:nat.eq C c2 (CSort n1))
             case CHead : c:C k0:K t:T 
                the thesis becomes 
                i:nat
                  .getl i (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
                    (or
                         ex2
                           C
                           λe:C.eq C c2 (CTail k u1 e)
                           λe:C.getl i (CHead c k0 t) (CHead e (Bind b) u2)
                         ex4
                           nat
                           λ:nat.eq nat i (clen (CHead c k0 t))
                           λ:nat.eq K k (Bind b)
                           λ:nat.eq T u1 u2
                           λn0:nat.eq C c2 (CSort n0))
                (H) by induction hypothesis we know 
                   i:nat
                     .getl i (CTail k u1 c) (CHead c2 (Bind b) u2)
                       (or
                            ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl i c (CHead e (Bind b) u2)
                            ex4
                              nat
                              λ:nat.eq nat i (clen c)
                              λ:nat.eq K k (Bind b)
                              λ:nat.eq T u1 u2
                              λn:nat.eq C c2 (CSort n))
                   assume inat
                      we proceed by induction on i to prove 
                         getl i (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
                           (or
                                ex2
                                  C
                                  λe:C.eq C c2 (CTail k u1 e)
                                  λe:C.getl i (CHead c k0 t) (CHead e (Bind b) u2)
                                ex4
                                  nat
                                  λ:nat.eq nat i (clen (CHead c k0 t))
                                  λ:nat.eq K k (Bind b)
                                  λ:nat.eq T u1 u2
                                  λn0:nat.eq C c2 (CSort n0))
                         case O : 
                            the thesis becomes 
                            getl O (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
                              (or
                                   ex2
                                     C
                                     λe:C.eq C c2 (CTail k u1 e)
                                     λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
                                   ex4
                                     nat
                                     λ:nat.eq nat O (clen (CHead c k0 t))
                                     λ:nat.eq K k (Bind b)
                                     λ:nat.eq T u1 u2
                                     λn0:nat.eq C c2 (CSort n0))
                               we must prove 
                                     getl O (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
                                       (or
                                            ex2
                                              C
                                              λe:C.eq C c2 (CTail k u1 e)
                                              λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
                                            ex4
                                              nat
                                              λ:nat.eq nat O (clen (CHead c k0 t))
                                              λ:nat.eq K k (Bind b)
                                              λ:nat.eq T u1 u2
                                              λn0:nat.eq C c2 (CSort n0))
                               or equivalently 
                                     getl O (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
                                       (or
                                            ex2
                                              C
                                              λe:C.eq C c2 (CTail k u1 e)
                                              λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
                                            ex4
                                              nat
                                              λ:nat.eq nat O (clen (CHead c k0 t))
                                              λ:nat.eq K k (Bind b)
                                              λ:nat.eq T u1 u2
                                              λn0:nat.eq C c2 (CSort n0))
                               suppose H0getl O (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
                                  by (getl_gen_O . . H0)
                                  we proved clear (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
                                     assume b0B
                                     suppose H1clear (CHead (CTail k u1 c) (Bind b0) t) (CHead c2 (Bind b) u2)
                                        (H2
                                           by (clear_gen_bind . . . . H1)
                                           we proved eq C (CHead c2 (Bind b) u2) (CHead (CTail k u1 c) (Bind b0) t)
                                           by (f_equal . . . . . previous)
                                           we proved 
                                              eq
                                                C
                                                <λ:C.C> CASE CHead c2 (Bind b) u2 OF CSort c2 | CHead c0  c0
                                                <λ:C.C> CASE CHead (CTail k u1 c) (Bind b0) t OF CSort c2 | CHead c0  c0

                                              eq
                                                C
                                                λe:C.<λ:C.C> CASE e OF CSort c2 | CHead c0  c0 (CHead c2 (Bind b) u2)
                                                λe:C.<λ:C.C> CASE e OF CSort c2 | CHead c0  c0
                                                  CHead (CTail k u1 c) (Bind b0) t
                                        end of H2
                                        (h1
                                           (H3
                                              by (clear_gen_bind . . . . H1)
                                              we proved eq C (CHead c2 (Bind b) u2) (CHead (CTail k u1 c) (Bind b0) t)
                                              by (f_equal . . . . . previous)
                                              we proved 
                                                 eq
                                                   B
                                                   <λ:C.B>
                                                     CASE CHead c2 (Bind b) u2 OF
                                                       CSort b
                                                     | CHead  k1 <λ:K.B> CASE k1 OF Bind b1b1 | Flat b
                                                   <λ:C.B>
                                                     CASE CHead (CTail k u1 c) (Bind b0) t OF
                                                       CSort b
                                                     | CHead  k1 <λ:K.B> CASE k1 OF Bind b1b1 | Flat b

                                                 eq
                                                   B
                                                   λe:C.<λ:C.B> CASE e OF CSort b | CHead  k1 <λ:K.B> CASE k1 OF Bind b1b1 | Flat b
                                                     CHead c2 (Bind b) u2
                                                   λe:C.<λ:C.B> CASE e OF CSort b | CHead  k1 <λ:K.B> CASE k1 OF Bind b1b1 | Flat b
                                                     CHead (CTail k u1 c) (Bind b0) t
                                           end of H3
                                           (h1
                                              (H4
                                                 by (clear_gen_bind . . . . H1)
                                                 we proved eq C (CHead c2 (Bind b) u2) (CHead (CTail k u1 c) (Bind b0) t)
                                                 by (f_equal . . . . . previous)
                                                 we proved 
                                                    eq
                                                      T
                                                      <λ:C.T> CASE CHead c2 (Bind b) u2 OF CSort u2 | CHead   t0t0
                                                      <λ:C.T> CASE CHead (CTail k u1 c) (Bind b0) t OF CSort u2 | CHead   t0t0

                                                    eq
                                                      T
                                                      λe:C.<λ:C.T> CASE e OF CSort u2 | CHead   t0t0 (CHead c2 (Bind b) u2)
                                                      λe:C.<λ:C.T> CASE e OF CSort u2 | CHead   t0t0
                                                        CHead (CTail k u1 c) (Bind b0) t
                                              end of H4
                                               suppose H5eq B b b0
                                               suppose H6eq C c2 (CTail k u1 c)
                                                 consider H4
                                                 we proved 
                                                    eq
                                                      T
                                                      <λ:C.T> CASE CHead c2 (Bind b) u2 OF CSort u2 | CHead   t0t0
                                                      <λ:C.T> CASE CHead (CTail k u1 c) (Bind b0) t OF CSort u2 | CHead   t0t0
                                                 that is equivalent to eq T u2 t
                                                 we proceed by induction on the previous result to prove 
                                                    or
                                                      ex2
                                                        C
                                                        λe:C.eq C c2 (CTail k u1 e)
                                                        λe:C.getl O (CHead c (Bind b0) t) (CHead e (Bind b) u2)
                                                      ex4
                                                        nat
                                                        λ:nat.eq nat O (s (Bind b0) (clen c))
                                                        λ:nat.eq K k (Bind b)
                                                        λ:nat.eq T u1 u2
                                                        λn:nat.eq C c2 (CSort n)
                                                    case refl_equal : 
                                                       the thesis becomes 
                                                       or
                                                         ex2
                                                           C
                                                           λe:C.eq C c2 (CTail k u1 e)
                                                           λe:C.getl O (CHead c (Bind b0) u2) (CHead e (Bind b) u2)
                                                         ex4
                                                           nat
                                                           λ:nat.eq nat O (s (Bind b0) (clen c))
                                                           λ:nat.eq K k (Bind b)
                                                           λ:nat.eq T u1 u2
                                                           λn:nat.eq C c2 (CSort n)
                                                          we proceed by induction on H5 to prove 
                                                             or
                                                               ex2
                                                                 C
                                                                 λe:C.eq C c2 (CTail k u1 e)
                                                                 λe:C.getl O (CHead c (Bind b0) u2) (CHead e (Bind b) u2)
                                                               ex4
                                                                 nat
                                                                 λ:nat.eq nat O (s (Bind b0) (clen c))
                                                                 λ:nat.eq K k (Bind b)
                                                                 λ:nat.eq T u1 u2
                                                                 λn:nat.eq C c2 (CSort n)
                                                             case refl_equal : 
                                                                the thesis becomes 
                                                                or
                                                                  ex2
                                                                    C
                                                                    λe:C.eq C c2 (CTail k u1 e)
                                                                    λe:C.getl O (CHead c (Bind b) u2) (CHead e (Bind b) u2)
                                                                  ex4
                                                                    nat
                                                                    λ:nat.eq nat O (s (Bind b) (clen c))
                                                                    λ:nat.eq K k (Bind b)
                                                                    λ:nat.eq T u1 u2
                                                                    λn:nat.eq C c2 (CSort n)
                                                                   (h1
                                                                      by (refl_equal . .)
eq C (CTail k u1 c) (CTail k u1 c)
                                                                   end of h1
                                                                   (h2
                                                                      by (getl_refl . . .)
getl O (CHead c (Bind b) u2) (CHead c (Bind b) u2)
                                                                   end of h2
                                                                   by (ex_intro2 . . . . h1 h2)
                                                                   we proved 
                                                                      ex2
                                                                        C
                                                                        λe:C.eq C (CTail k u1 c) (CTail k u1 e)
                                                                        λe:C.getl O (CHead c (Bind b) u2) (CHead e (Bind b) u2)
                                                                   by (or_introl . . previous)
                                                                   we proved 
                                                                      or
                                                                        ex2
                                                                          C
                                                                          λe:C.eq C (CTail k u1 c) (CTail k u1 e)
                                                                          λe:C.getl O (CHead c (Bind b) u2) (CHead e (Bind b) u2)
                                                                        ex4
                                                                          nat
                                                                          λ:nat.eq nat O (s (Bind b) (clen c))
                                                                          λ:nat.eq K k (Bind b)
                                                                          λ:nat.eq T u1 u2
                                                                          λn:nat.eq C (CTail k u1 c) (CSort n)
                                                                   by (eq_ind_r . . . previous . H6)

                                                                      or
                                                                        ex2
                                                                          C
                                                                          λe:C.eq C c2 (CTail k u1 e)
                                                                          λe:C.getl O (CHead c (Bind b) u2) (CHead e (Bind b) u2)
                                                                        ex4
                                                                          nat
                                                                          λ:nat.eq nat O (s (Bind b) (clen c))
                                                                          λ:nat.eq K k (Bind b)
                                                                          λ:nat.eq T u1 u2
                                                                          λn:nat.eq C c2 (CSort n)

                                                             or
                                                               ex2
                                                                 C
                                                                 λe:C.eq C c2 (CTail k u1 e)
                                                                 λe:C.getl O (CHead c (Bind b0) u2) (CHead e (Bind b) u2)
                                                               ex4
                                                                 nat
                                                                 λ:nat.eq nat O (s (Bind b0) (clen c))
                                                                 λ:nat.eq K k (Bind b)
                                                                 λ:nat.eq T u1 u2
                                                                 λn:nat.eq C c2 (CSort n)
                                                 we proved 
                                                    or
                                                      ex2
                                                        C
                                                        λe:C.eq C c2 (CTail k u1 e)
                                                        λe:C.getl O (CHead c (Bind b0) t) (CHead e (Bind b) u2)
                                                      ex4
                                                        nat
                                                        λ:nat.eq nat O (s (Bind b0) (clen c))
                                                        λ:nat.eq K k (Bind b)
                                                        λ:nat.eq T u1 u2
                                                        λn:nat.eq C c2 (CSort n)

                                                 eq B b b0
                                                   (eq C c2 (CTail k u1 c)
                                                        (or
                                                             ex2
                                                               C
                                                               λe:C.eq C c2 (CTail k u1 e)
                                                               λe:C.getl O (CHead c (Bind b0) t) (CHead e (Bind b) u2)
                                                             ex4
                                                               nat
                                                               λ:nat.eq nat O (s (Bind b0) (clen c))
                                                               λ:nat.eq K k (Bind b)
                                                               λ:nat.eq T u1 u2
                                                               λn:nat.eq C c2 (CSort n)))
                                           end of h1
                                           (h2
                                              consider H3
                                              we proved 
                                                 eq
                                                   B
                                                   <λ:C.B>
                                                     CASE CHead c2 (Bind b) u2 OF
                                                       CSort b
                                                     | CHead  k1 <λ:K.B> CASE k1 OF Bind b1b1 | Flat b
                                                   <λ:C.B>
                                                     CASE CHead (CTail k u1 c) (Bind b0) t OF
                                                       CSort b
                                                     | CHead  k1 <λ:K.B> CASE k1 OF Bind b1b1 | Flat b
eq B b b0
                                           end of h2
                                           by (h1 h2)

                                              eq C c2 (CTail k u1 c)
                                                (or
                                                     ex2
                                                       C
                                                       λe:C.eq C c2 (CTail k u1 e)
                                                       λe:C.getl O (CHead c (Bind b0) t) (CHead e (Bind b) u2)
                                                     ex4
                                                       nat
                                                       λ:nat.eq nat O (s (Bind b0) (clen c))
                                                       λ:nat.eq K k (Bind b)
                                                       λ:nat.eq T u1 u2
                                                       λn:nat.eq C c2 (CSort n))
                                        end of h1
                                        (h2
                                           consider H2
                                           we proved 
                                              eq
                                                C
                                                <λ:C.C> CASE CHead c2 (Bind b) u2 OF CSort c2 | CHead c0  c0
                                                <λ:C.C> CASE CHead (CTail k u1 c) (Bind b0) t OF CSort c2 | CHead c0  c0
eq C c2 (CTail k u1 c)
                                        end of h2
                                        by (h1 h2)
                                        we proved 
                                           or
                                             ex2
                                               C
                                               λe:C.eq C c2 (CTail k u1 e)
                                               λe:C.getl O (CHead c (Bind b0) t) (CHead e (Bind b) u2)
                                             ex4
                                               nat
                                               λ:nat.eq nat O (s (Bind b0) (clen c))
                                               λ:nat.eq K k (Bind b)
                                               λ:nat.eq T u1 u2
                                               λn:nat.eq C c2 (CSort n)

                                        H1:clear (CHead (CTail k u1 c) (Bind b0) t) (CHead c2 (Bind b) u2)
                                          .or
                                            ex2
                                              C
                                              λe:C.eq C c2 (CTail k u1 e)
                                              λe:C.getl O (CHead c (Bind b0) t) (CHead e (Bind b) u2)
                                            ex4
                                              nat
                                              λ:nat.eq nat O (s (Bind b0) (clen c))
                                              λ:nat.eq K k (Bind b)
                                              λ:nat.eq T u1 u2
                                              λn:nat.eq C c2 (CSort n)
                                     assume fF
                                     suppose H1clear (CHead (CTail k u1 c) (Flat f) t) (CHead c2 (Bind b) u2)
                                        (H2
                                           (h1
                                              by (drop_refl .)
drop O O (CTail k u1 c) (CTail k u1 c)
                                           end of h1
                                           (h2
                                              by (clear_gen_flat . . . . H1)
clear (CTail k u1 c) (CHead c2 (Bind b) u2)
                                           end of h2
                                           by (getl_intro . . . . h1 h2)
                                           we proved getl O (CTail k u1 c) (CHead c2 (Bind b) u2)
                                           by (H . previous)

                                              or
                                                ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl O c (CHead e (Bind b) u2)
                                                ex4
                                                  nat
                                                  λ:nat.eq nat O (clen c)
                                                  λ:nat.eq K k (Bind b)
                                                  λ:nat.eq T u1 u2
                                                  λn:nat.eq C c2 (CSort n)
                                        end of H2
                                        we proceed by induction on H2 to prove 
                                           or
                                             ex2
                                               C
                                               λe:C.eq C c2 (CTail k u1 e)
                                               λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                             ex4
                                               nat
                                               λ:nat.eq nat O (s (Flat f) (clen c))
                                               λ:nat.eq K k (Bind b)
                                               λ:nat.eq T u1 u2
                                               λn:nat.eq C c2 (CSort n)
                                           case or_introl : H3:ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl O c (CHead e (Bind b) u2) 
                                              the thesis becomes 
                                              or
                                                ex2
                                                  C
                                                  λe:C.eq C c2 (CTail k u1 e)
                                                  λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                ex4
                                                  nat
                                                  λ:nat.eq nat O (s (Flat f) (clen c))
                                                  λ:nat.eq K k (Bind b)
                                                  λ:nat.eq T u1 u2
                                                  λn:nat.eq C c2 (CSort n)
                                                 we proceed by induction on H3 to prove 
                                                    or
                                                      ex2
                                                        C
                                                        λe:C.eq C c2 (CTail k u1 e)
                                                        λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                      ex4
                                                        nat
                                                        λ:nat.eq nat O (s (Flat f) (clen c))
                                                        λ:nat.eq K k (Bind b)
                                                        λ:nat.eq T u1 u2
                                                        λn:nat.eq C c2 (CSort n)
                                                    case ex_intro2 : x:C H4:eq C c2 (CTail k u1 x) H5:getl O c (CHead x (Bind b) u2) 
                                                       the thesis becomes 
                                                       or
                                                         ex2
                                                           C
                                                           λe:C.eq C c2 (CTail k u1 e)
                                                           λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                         ex4
                                                           nat
                                                           λ:nat.eq nat O (s (Flat f) (clen c))
                                                           λ:nat.eq K k (Bind b)
                                                           λ:nat.eq T u1 u2
                                                           λn:nat.eq C c2 (CSort n)
                                                          (h1
                                                             by (refl_equal . .)
eq C (CTail k u1 x) (CTail k u1 x)
                                                          end of h1
                                                          (h2
                                                             by (getl_flat . . . H5 . .)
getl O (CHead c (Flat f) t) (CHead x (Bind b) u2)
                                                          end of h2
                                                          by (ex_intro2 . . . . h1 h2)
                                                          we proved 
                                                             ex2
                                                               C
                                                               λe:C.eq C (CTail k u1 x) (CTail k u1 e)
                                                               λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                          by (or_introl . . previous)
                                                          we proved 
                                                             or
                                                               ex2
                                                                 C
                                                                 λe:C.eq C (CTail k u1 x) (CTail k u1 e)
                                                                 λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                               ex4
                                                                 nat
                                                                 λ:nat.eq nat O (s (Flat f) (clen c))
                                                                 λ:nat.eq K k (Bind b)
                                                                 λ:nat.eq T u1 u2
                                                                 λn:nat.eq C (CTail k u1 x) (CSort n)
                                                          by (eq_ind_r . . . previous . H4)

                                                             or
                                                               ex2
                                                                 C
                                                                 λe:C.eq C c2 (CTail k u1 e)
                                                                 λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                               ex4
                                                                 nat
                                                                 λ:nat.eq nat O (s (Flat f) (clen c))
                                                                 λ:nat.eq K k (Bind b)
                                                                 λ:nat.eq T u1 u2
                                                                 λn:nat.eq C c2 (CSort n)

                                                    or
                                                      ex2
                                                        C
                                                        λe:C.eq C c2 (CTail k u1 e)
                                                        λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                      ex4
                                                        nat
                                                        λ:nat.eq nat O (s (Flat f) (clen c))
                                                        λ:nat.eq K k (Bind b)
                                                        λ:nat.eq T u1 u2
                                                        λn:nat.eq C c2 (CSort n)
                                           case or_intror : H3:ex4 nat λ:nat.eq nat O (clen c) λ:nat.eq K k (Bind b) λ:nat.eq T u1 u2 λn:nat.eq C c2 (CSort n) 
                                              the thesis becomes 
                                              or
                                                ex2
                                                  C
                                                  λe:C.eq C c2 (CTail k u1 e)
                                                  λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                ex4
                                                  nat
                                                  λ:nat.eq nat O (s (Flat f) (clen c))
                                                  λ:nat.eq K k (Bind b)
                                                  λ:nat.eq T u1 u2
                                                  λn:nat.eq C c2 (CSort n)
                                                 we proceed by induction on H3 to prove 
                                                    or
                                                      ex2
                                                        C
                                                        λe:C.eq C c2 (CTail k u1 e)
                                                        λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                      ex4
                                                        nat
                                                        λ:nat.eq nat O (s (Flat f) (clen c))
                                                        λ:nat.eq K k (Bind b)
                                                        λ:nat.eq T u1 u2
                                                        λn:nat.eq C c2 (CSort n)
                                                    case ex4_intro : x0:nat H4:eq nat O (clen c) H5:eq K k (Bind b) H6:eq T u1 u2 H7:eq C c2 (CSort x0) 
                                                       the thesis becomes 
                                                       or
                                                         ex2
                                                           C
                                                           λe:C.eq C c2 (CTail k u1 e)
                                                           λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                         ex4
                                                           nat
                                                           λ:nat.eq nat O (s (Flat f) (clen c))
                                                           λ:nat.eq K k (Bind b)
                                                           λ:nat.eq T u1 u2
                                                           λn:nat.eq C c2 (CSort n)
                                                          we proceed by induction on H6 to prove 
                                                             or
                                                               ex2
                                                                 C
                                                                 λe:C.eq C (CSort x0) (CTail k u1 e)
                                                                 λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                               ex4
                                                                 nat
                                                                 λ:nat.eq nat O (s (Flat f) (clen c))
                                                                 λ:nat.eq K k (Bind b)
                                                                 λ:nat.eq T u1 u2
                                                                 λn:nat.eq C (CSort x0) (CSort n)
                                                             case refl_equal : 
                                                                the thesis becomes 
                                                                or
                                                                  ex2
                                                                    C
                                                                    λe:C.eq C (CSort x0) (CTail k u1 e)
                                                                    λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u1)
                                                                  ex4
                                                                    nat
                                                                    λ:nat.eq nat O (s (Flat f) (clen c))
                                                                    λ:nat.eq K k (Bind b)
                                                                    λ:nat.eq T u1 u1
                                                                    λn:nat.eq C (CSort x0) (CSort n)
                                                                   (h1
                                                                      consider H4
                                                                      we proved eq nat O (clen c)
eq nat O (s (Flat f) (clen c))
                                                                   end of h1
                                                                   (h2
                                                                      by (refl_equal . .)
eq K (Bind b) (Bind b)
                                                                   end of h2
                                                                   (h3
                                                                      by (refl_equal . .)
eq T u1 u1
                                                                   end of h3
                                                                   (h4
                                                                      by (refl_equal . .)
eq C (CSort x0) (CSort x0)
                                                                   end of h4
                                                                   by (ex4_intro . . . . . . h1 h2 h3 h4)
                                                                   we proved 
                                                                      ex4
                                                                        nat
                                                                        λ:nat.eq nat O (s (Flat f) (clen c))
                                                                        λ:nat.eq K (Bind b) (Bind b)
                                                                        λ:nat.eq T u1 u1
                                                                        λn:nat.eq C (CSort x0) (CSort n)
                                                                   by (or_intror . . previous)
                                                                   we proved 
                                                                      or
                                                                        ex2
                                                                          C
                                                                          λe:C.eq C (CSort x0) (CTail (Bind b) u1 e)
                                                                          λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u1)
                                                                        ex4
                                                                          nat
                                                                          λ:nat.eq nat O (s (Flat f) (clen c))
                                                                          λ:nat.eq K (Bind b) (Bind b)
                                                                          λ:nat.eq T u1 u1
                                                                          λn:nat.eq C (CSort x0) (CSort n)
                                                                   by (eq_ind_r . . . previous . H5)

                                                                      or
                                                                        ex2
                                                                          C
                                                                          λe:C.eq C (CSort x0) (CTail k u1 e)
                                                                          λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u1)
                                                                        ex4
                                                                          nat
                                                                          λ:nat.eq nat O (s (Flat f) (clen c))
                                                                          λ:nat.eq K k (Bind b)
                                                                          λ:nat.eq T u1 u1
                                                                          λn:nat.eq C (CSort x0) (CSort n)
                                                          we proved 
                                                             or
                                                               ex2
                                                                 C
                                                                 λe:C.eq C (CSort x0) (CTail k u1 e)
                                                                 λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                               ex4
                                                                 nat
                                                                 λ:nat.eq nat O (s (Flat f) (clen c))
                                                                 λ:nat.eq K k (Bind b)
                                                                 λ:nat.eq T u1 u2
                                                                 λn:nat.eq C (CSort x0) (CSort n)
                                                          by (eq_ind_r . . . previous . H7)

                                                             or
                                                               ex2
                                                                 C
                                                                 λe:C.eq C c2 (CTail k u1 e)
                                                                 λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                               ex4
                                                                 nat
                                                                 λ:nat.eq nat O (s (Flat f) (clen c))
                                                                 λ:nat.eq K k (Bind b)
                                                                 λ:nat.eq T u1 u2
                                                                 λn:nat.eq C c2 (CSort n)

                                                    or
                                                      ex2
                                                        C
                                                        λe:C.eq C c2 (CTail k u1 e)
                                                        λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                                      ex4
                                                        nat
                                                        λ:nat.eq nat O (s (Flat f) (clen c))
                                                        λ:nat.eq K k (Bind b)
                                                        λ:nat.eq T u1 u2
                                                        λn:nat.eq C c2 (CSort n)
                                        we proved 
                                           or
                                             ex2
                                               C
                                               λe:C.eq C c2 (CTail k u1 e)
                                               λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                             ex4
                                               nat
                                               λ:nat.eq nat O (s (Flat f) (clen c))
                                               λ:nat.eq K k (Bind b)
                                               λ:nat.eq T u1 u2
                                               λn:nat.eq C c2 (CSort n)

                                        H1:clear (CHead (CTail k u1 c) (Flat f) t) (CHead c2 (Bind b) u2)
                                          .or
                                            ex2
                                              C
                                              λe:C.eq C c2 (CTail k u1 e)
                                              λe:C.getl O (CHead c (Flat f) t) (CHead e (Bind b) u2)
                                            ex4
                                              nat
                                              λ:nat.eq nat O (s (Flat f) (clen c))
                                              λ:nat.eq K k (Bind b)
                                              λ:nat.eq T u1 u2
                                              λn:nat.eq C c2 (CSort n)
                                  by (previous . previous)
                                  we proved 
                                     or
                                       ex2
                                         C
                                         λe:C.eq C c2 (CTail k u1 e)
                                         λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
                                       ex4
                                         nat
                                         λ:nat.eq nat O (s k0 (clen c))
                                         λ:nat.eq K k (Bind b)
                                         λ:nat.eq T u1 u2
                                         λn:nat.eq C c2 (CSort n)
                                  that is equivalent to 
                                     or
                                       ex2
                                         C
                                         λe:C.eq C c2 (CTail k u1 e)
                                         λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
                                       ex4
                                         nat
                                         λ:nat.eq nat O (clen (CHead c k0 t))
                                         λ:nat.eq K k (Bind b)
                                         λ:nat.eq T u1 u2
                                         λn0:nat.eq C c2 (CSort n0)
                               we proved 
                                  getl O (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
                                    (or
                                         ex2
                                           C
                                           λe:C.eq C c2 (CTail k u1 e)
                                           λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
                                         ex4
                                           nat
                                           λ:nat.eq nat O (clen (CHead c k0 t))
                                           λ:nat.eq K k (Bind b)
                                           λ:nat.eq T u1 u2
                                           λn0:nat.eq C c2 (CSort n0))

                                  getl O (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
                                    (or
                                         ex2
                                           C
                                           λe:C.eq C c2 (CTail k u1 e)
                                           λe:C.getl O (CHead c k0 t) (CHead e (Bind b) u2)
                                         ex4
                                           nat
                                           λ:nat.eq nat O (clen (CHead c k0 t))
                                           λ:nat.eq K k (Bind b)
                                           λ:nat.eq T u1 u2
                                           λn0:nat.eq C c2 (CSort n0))
                         case S : n:nat 
                            the thesis becomes 
                            getl (S n) (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
                              (or
                                   ex2
                                     C
                                     λe:C.eq C c2 (CTail k u1 e)
                                     λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                   ex4
                                     nat
                                     λ:nat.eq nat (S n) (clen (CHead c k0 t))
                                     λ:nat.eq K k (Bind b)
                                     λ:nat.eq T u1 u2
                                     λn0:nat.eq C c2 (CSort n0))
                            (H0) by induction hypothesis we know 
                               getl n (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
                                 (or
                                      ex2
                                        C
                                        λe:C.eq C c2 (CTail k u1 e)
                                        λe:C.getl n (CHead c k0 t) (CHead e (Bind b) u2)
                                      ex4
                                        nat
                                        λ:nat.eq nat n (s k0 (clen c))
                                        λ:nat.eq K k (Bind b)
                                        λ:nat.eq T u1 u2
                                        λn0:nat.eq C c2 (CSort n0))
                               we must prove 
                                     getl (S n) (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
                                       (or
                                            ex2
                                              C
                                              λe:C.eq C c2 (CTail k u1 e)
                                              λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                            ex4
                                              nat
                                              λ:nat.eq nat (S n) (clen (CHead c k0 t))
                                              λ:nat.eq K k (Bind b)
                                              λ:nat.eq T u1 u2
                                              λn0:nat.eq C c2 (CSort n0))
                               or equivalently 
                                     getl (S n) (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
                                       (or
                                            ex2
                                              C
                                              λe:C.eq C c2 (CTail k u1 e)
                                              λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                            ex4
                                              nat
                                              λ:nat.eq nat (S n) (clen (CHead c k0 t))
                                              λ:nat.eq K k (Bind b)
                                              λ:nat.eq T u1 u2
                                              λn0:nat.eq C c2 (CSort n0))
                               suppose H1getl (S n) (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
                                  (H_x
                                     by (getl_gen_S . . . . . H1)
                                     we proved getl (r k0 n) (CTail k u1 c) (CHead c2 (Bind b) u2)
                                     by (H . previous)

                                        or
                                          ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl (r k0 n) c (CHead e (Bind b) u2)
                                          ex4
                                            nat
                                            λ:nat.eq nat (r k0 n) (clen c)
                                            λ:nat.eq K k (Bind b)
                                            λ:nat.eq T u1 u2
                                            λn:nat.eq C c2 (CSort n)
                                  end of H_x
                                  (H2consider H_x
                                  we proceed by induction on H2 to prove 
                                     or
                                       ex2
                                         C
                                         λe:C.eq C c2 (CTail k u1 e)
                                         λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                       ex4
                                         nat
                                         λ:nat.eq nat (S n) (s k0 (clen c))
                                         λ:nat.eq K k (Bind b)
                                         λ:nat.eq T u1 u2
                                         λn0:nat.eq C c2 (CSort n0)
                                     case or_introl : H3:ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl (r k0 n) c (CHead e (Bind b) u2) 
                                        the thesis becomes 
                                        or
                                          ex2
                                            C
                                            λe:C.eq C c2 (CTail k u1 e)
                                            λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                          ex4
                                            nat
                                            λ:nat.eq nat (S n) (s k0 (clen c))
                                            λ:nat.eq K k (Bind b)
                                            λ:nat.eq T u1 u2
                                            λn0:nat.eq C c2 (CSort n0)
                                           we proceed by induction on H3 to prove 
                                              or
                                                ex2
                                                  C
                                                  λe:C.eq C c2 (CTail k u1 e)
                                                  λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                                ex4
                                                  nat
                                                  λ:nat.eq nat (S n) (s k0 (clen c))
                                                  λ:nat.eq K k (Bind b)
                                                  λ:nat.eq T u1 u2
                                                  λn0:nat.eq C c2 (CSort n0)
                                              case ex_intro2 : x:C H4:eq C c2 (CTail k u1 x) H5:getl (r k0 n) c (CHead x (Bind b) u2) 
                                                 the thesis becomes 
                                                 or
                                                   ex2
                                                     C
                                                     λe:C.eq C c2 (CTail k u1 e)
                                                     λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                                   ex4
                                                     nat
                                                     λ:nat.eq nat (S n) (s k0 (clen c))
                                                     λ:nat.eq K k (Bind b)
                                                     λ:nat.eq T u1 u2
                                                     λn0:nat.eq C c2 (CSort n0)
                                                    (h1
                                                       by (refl_equal . .)
eq C (CTail k u1 x) (CTail k u1 x)
                                                    end of h1
                                                    (h2
                                                       by (getl_head . . . . H5 .)
getl (S n) (CHead c k0 t) (CHead x (Bind b) u2)
                                                    end of h2
                                                    by (ex_intro2 . . . . h1 h2)
                                                    we proved 
                                                       ex2
                                                         C
                                                         λe:C.eq C (CTail k u1 x) (CTail k u1 e)
                                                         λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                                    by (or_introl . . previous)
                                                    we proved 
                                                       or
                                                         ex2
                                                           C
                                                           λe:C.eq C (CTail k u1 x) (CTail k u1 e)
                                                           λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                                         ex4
                                                           nat
                                                           λ:nat.eq nat (S n) (s k0 (clen c))
                                                           λ:nat.eq K k (Bind b)
                                                           λ:nat.eq T u1 u2
                                                           λn0:nat.eq C (CTail k u1 x) (CSort n0)
                                                    by (eq_ind_r . . . previous . H4)

                                                       or
                                                         ex2
                                                           C
                                                           λe:C.eq C c2 (CTail k u1 e)
                                                           λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                                         ex4
                                                           nat
                                                           λ:nat.eq nat (S n) (s k0 (clen c))
                                                           λ:nat.eq K k (Bind b)
                                                           λ:nat.eq T u1 u2
                                                           λn0:nat.eq C c2 (CSort n0)

                                              or
                                                ex2
                                                  C
                                                  λe:C.eq C c2 (CTail k u1 e)
                                                  λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                                ex4
                                                  nat
                                                  λ:nat.eq nat (S n) (s k0 (clen c))
                                                  λ:nat.eq K k (Bind b)
                                                  λ:nat.eq T u1 u2
                                                  λn0:nat.eq C c2 (CSort n0)
                                     case or_intror : H3:ex4 nat λ:nat.eq nat (r k0 n) (clen c) λ:nat.eq K k (Bind b) λ:nat.eq T u1 u2 λn0:nat.eq C c2 (CSort n0) 
                                        the thesis becomes 
                                        or
                                          ex2
                                            C
                                            λe:C.eq C c2 (CTail k u1 e)
                                            λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                          ex4
                                            nat
                                            λ:nat.eq nat (S n) (s k0 (clen c))
                                            λ:nat.eq K k (Bind b)
                                            λ:nat.eq T u1 u2
                                            λn0:nat.eq C c2 (CSort n0)
                                           we proceed by induction on H3 to prove 
                                              or
                                                ex2
                                                  C
                                                  λe:C.eq C c2 (CTail k u1 e)
                                                  λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                                ex4
                                                  nat
                                                  λ:nat.eq nat (S n) (s k0 (clen c))
                                                  λ:nat.eq K k (Bind b)
                                                  λ:nat.eq T u1 u2
                                                  λn0:nat.eq C c2 (CSort n0)
                                              case ex4_intro : x0:nat H4:eq nat (r k0 n) (clen c) H5:eq K k (Bind b) H6:eq T u1 u2 H7:eq C c2 (CSort x0) 
                                                 the thesis becomes 
                                                 or
                                                   ex2
                                                     C
                                                     λe:C.eq C c2 (CTail k u1 e)
                                                     λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                                   ex4
                                                     nat
                                                     λ:nat.eq nat (S n) (s k0 (clen c))
                                                     λ:nat.eq K k (Bind b)
                                                     λ:nat.eq T u1 u2
                                                     λn0:nat.eq C c2 (CSort n0)
                                                    (H8
                                                       we proceed by induction on H7 to prove getl (r k0 n) (CTail k u1 c) (CHead (CSort x0) (Bind b) u2)
                                                          case refl_equal : 
                                                             the thesis becomes getl (r k0 n) (CTail k u1 c) (CHead c2 (Bind b) u2)
                                                                by (getl_gen_S . . . . . H1)
getl (r k0 n) (CTail k u1 c) (CHead c2 (Bind b) u2)
getl (r k0 n) (CTail k u1 c) (CHead (CSort x0) (Bind b) u2)
                                                    end of H8
                                                    (H9
                                                       we proceed by induction on H7 to prove 
                                                          getl n (CHead (CTail k u1 c) k0 t) (CHead (CSort x0) (Bind b) u2)
                                                            (or
                                                                 ex2
                                                                   C
                                                                   λe:C.eq C (CSort x0) (CTail k u1 e)
                                                                   λe:C.getl n (CHead c k0 t) (CHead e (Bind b) u2)
                                                                 ex4
                                                                   nat
                                                                   λ:nat.eq nat n (s k0 (clen c))
                                                                   λ:nat.eq K k (Bind b)
                                                                   λ:nat.eq T u1 u2
                                                                   λn0:nat.eq C (CSort x0) (CSort n0))
                                                          case refl_equal : 
                                                             the thesis becomes the hypothesis H0

                                                          getl n (CHead (CTail k u1 c) k0 t) (CHead (CSort x0) (Bind b) u2)
                                                            (or
                                                                 ex2
                                                                   C
                                                                   λe:C.eq C (CSort x0) (CTail k u1 e)
                                                                   λe:C.getl n (CHead c k0 t) (CHead e (Bind b) u2)
                                                                 ex4
                                                                   nat
                                                                   λ:nat.eq nat n (s k0 (clen c))
                                                                   λ:nat.eq K k (Bind b)
                                                                   λ:nat.eq T u1 u2
                                                                   λn0:nat.eq C (CSort x0) (CSort n0))
                                                    end of H9
                                                    (H10
                                                       by (eq_ind_r . . . H9 . H6)

                                                          getl n (CHead (CTail k u1 c) k0 t) (CHead (CSort x0) (Bind b) u1)
                                                            (or
                                                                 ex2
                                                                   C
                                                                   λe:C.eq C (CSort x0) (CTail k u1 e)
                                                                   λe:C.getl n (CHead c k0 t) (CHead e (Bind b) u1)
                                                                 ex4
                                                                   nat
                                                                   λ:nat.eq nat n (s k0 (clen c))
                                                                   λ:nat.eq K k (Bind b)
                                                                   λ:nat.eq T u1 u1
                                                                   λn0:nat.eq C (CSort x0) (CSort n0))
                                                    end of H10
                                                    (H11
                                                       by (eq_ind_r . . . H8 . H6)
getl (r k0 n) (CTail k u1 c) (CHead (CSort x0) (Bind b) u1)
                                                    end of H11
                                                    we proceed by induction on H6 to prove 
                                                       or
                                                         ex2
                                                           C
                                                           λe:C.eq C (CSort x0) (CTail k u1 e)
                                                           λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                                         ex4
                                                           nat
                                                           λ:nat.eq nat (S n) (s k0 (clen c))
                                                           λ:nat.eq K k (Bind b)
                                                           λ:nat.eq T u1 u2
                                                           λn0:nat.eq C (CSort x0) (CSort n0)
                                                       case refl_equal : 
                                                          the thesis becomes 
                                                          or
                                                            ex2
                                                              C
                                                              λe:C.eq C (CSort x0) (CTail k u1 e)
                                                              λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
                                                            ex4
                                                              nat
                                                              λ:nat.eq nat (S n) (s k0 (clen c))
                                                              λ:nat.eq K k (Bind b)
                                                              λ:nat.eq T u1 u1
                                                              λn0:nat.eq C (CSort x0) (CSort n0)
                                                             we proceed by induction on H4 to prove 
                                                                or
                                                                  ex2
                                                                    C
                                                                    λe:C.eq C (CSort x0) (CTail (Bind b) u1 e)
                                                                    λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
                                                                  ex4
                                                                    nat
                                                                    λ:nat.eq nat (S n) (s k0 (clen c))
                                                                    λ:nat.eq K (Bind b) (Bind b)
                                                                    λ:nat.eq T u1 u1
                                                                    λn1:nat.eq C (CSort x0) (CSort n1)
                                                                case refl_equal : 
                                                                   the thesis becomes 
                                                                   or
                                                                     ex2
                                                                       C
                                                                       λe:C.eq C (CSort x0) (CTail (Bind b) u1 e)
                                                                       λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
                                                                     ex4
                                                                       nat
                                                                       λ:nat.eq nat (S n) (s k0 (r k0 n))
                                                                       λ:nat.eq K (Bind b) (Bind b)
                                                                       λ:nat.eq T u1 u1
                                                                       λn1:nat.eq C (CSort x0) (CSort n1)
                                                                      (h1
                                                                         (h1
                                                                            by (refl_equal . .)
eq nat (S n) (S n)
                                                                         end of h1
                                                                         (h2
                                                                            by (refl_equal . .)
eq K (Bind b) (Bind b)
                                                                         end of h2
                                                                         (h3
                                                                            by (refl_equal . .)
eq T u1 u1
                                                                         end of h3
                                                                         (h4
                                                                            by (refl_equal . .)
eq C (CSort x0) (CSort x0)
                                                                         end of h4
                                                                         by (ex4_intro . . . . . . h1 h2 h3 h4)
                                                                         we proved 
                                                                            ex4
                                                                              nat
                                                                              λ:nat.eq nat (S n) (S n)
                                                                              λ:nat.eq K (Bind b) (Bind b)
                                                                              λ:nat.eq T u1 u1
                                                                              λn0:nat.eq C (CSort x0) (CSort n0)
                                                                         by (or_intror . . previous)

                                                                            or
                                                                              ex2
                                                                                C
                                                                                λe:C.eq C (CSort x0) (CTail (Bind b) u1 e)
                                                                                λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
                                                                              ex4
                                                                                nat
                                                                                λ:nat.eq nat (S n) (S n)
                                                                                λ:nat.eq K (Bind b) (Bind b)
                                                                                λ:nat.eq T u1 u1
                                                                                λn0:nat.eq C (CSort x0) (CSort n0)
                                                                      end of h1
                                                                      (h2
                                                                         by (s_r . .)
eq nat (s k0 (r k0 n)) (S n)
                                                                      end of h2
                                                                      by (eq_ind_r . . . h1 . h2)

                                                                         or
                                                                           ex2
                                                                             C
                                                                             λe:C.eq C (CSort x0) (CTail (Bind b) u1 e)
                                                                             λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
                                                                           ex4
                                                                             nat
                                                                             λ:nat.eq nat (S n) (s k0 (r k0 n))
                                                                             λ:nat.eq K (Bind b) (Bind b)
                                                                             λ:nat.eq T u1 u1
                                                                             λn1:nat.eq C (CSort x0) (CSort n1)
                                                             we proved 
                                                                or
                                                                  ex2
                                                                    C
                                                                    λe:C.eq C (CSort x0) (CTail (Bind b) u1 e)
                                                                    λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
                                                                  ex4
                                                                    nat
                                                                    λ:nat.eq nat (S n) (s k0 (clen c))
                                                                    λ:nat.eq K (Bind b) (Bind b)
                                                                    λ:nat.eq T u1 u1
                                                                    λn1:nat.eq C (CSort x0) (CSort n1)
                                                             by (eq_ind_r . . . previous . H5)

                                                                or
                                                                  ex2
                                                                    C
                                                                    λe:C.eq C (CSort x0) (CTail k u1 e)
                                                                    λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)
                                                                  ex4
                                                                    nat
                                                                    λ:nat.eq nat (S n) (s k0 (clen c))
                                                                    λ:nat.eq K k (Bind b)
                                                                    λ:nat.eq T u1 u1
                                                                    λn0:nat.eq C (CSort x0) (CSort n0)
                                                    we proved 
                                                       or
                                                         ex2
                                                           C
                                                           λe:C.eq C (CSort x0) (CTail k u1 e)
                                                           λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                                         ex4
                                                           nat
                                                           λ:nat.eq nat (S n) (s k0 (clen c))
                                                           λ:nat.eq K k (Bind b)
                                                           λ:nat.eq T u1 u2
                                                           λn0:nat.eq C (CSort x0) (CSort n0)
                                                    by (eq_ind_r . . . previous . H7)

                                                       or
                                                         ex2
                                                           C
                                                           λe:C.eq C c2 (CTail k u1 e)
                                                           λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                                         ex4
                                                           nat
                                                           λ:nat.eq nat (S n) (s k0 (clen c))
                                                           λ:nat.eq K k (Bind b)
                                                           λ:nat.eq T u1 u2
                                                           λn0:nat.eq C c2 (CSort n0)

                                              or
                                                ex2
                                                  C
                                                  λe:C.eq C c2 (CTail k u1 e)
                                                  λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                                ex4
                                                  nat
                                                  λ:nat.eq nat (S n) (s k0 (clen c))
                                                  λ:nat.eq K k (Bind b)
                                                  λ:nat.eq T u1 u2
                                                  λn0:nat.eq C c2 (CSort n0)
                                  we proved 
                                     or
                                       ex2
                                         C
                                         λe:C.eq C c2 (CTail k u1 e)
                                         λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                       ex4
                                         nat
                                         λ:nat.eq nat (S n) (s k0 (clen c))
                                         λ:nat.eq K k (Bind b)
                                         λ:nat.eq T u1 u2
                                         λn0:nat.eq C c2 (CSort n0)
                                  that is equivalent to 
                                     or
                                       ex2
                                         C
                                         λe:C.eq C c2 (CTail k u1 e)
                                         λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                       ex4
                                         nat
                                         λ:nat.eq nat (S n) (clen (CHead c k0 t))
                                         λ:nat.eq K k (Bind b)
                                         λ:nat.eq T u1 u2
                                         λn0:nat.eq C c2 (CSort n0)
                               we proved 
                                  getl (S n) (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)
                                    (or
                                         ex2
                                           C
                                           λe:C.eq C c2 (CTail k u1 e)
                                           λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                         ex4
                                           nat
                                           λ:nat.eq nat (S n) (clen (CHead c k0 t))
                                           λ:nat.eq K k (Bind b)
                                           λ:nat.eq T u1 u2
                                           λn0:nat.eq C c2 (CSort n0))

                                  getl (S n) (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
                                    (or
                                         ex2
                                           C
                                           λe:C.eq C c2 (CTail k u1 e)
                                           λe:C.getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)
                                         ex4
                                           nat
                                           λ:nat.eq nat (S n) (clen (CHead c k0 t))
                                           λ:nat.eq K k (Bind b)
                                           λ:nat.eq T u1 u2
                                           λn0:nat.eq C c2 (CSort n0))
                      we proved 
                         getl i (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
                           (or
                                ex2
                                  C
                                  λe:C.eq C c2 (CTail k u1 e)
                                  λe:C.getl i (CHead c k0 t) (CHead e (Bind b) u2)
                                ex4
                                  nat
                                  λ:nat.eq nat i (clen (CHead c k0 t))
                                  λ:nat.eq K k (Bind b)
                                  λ:nat.eq T u1 u2
                                  λn0:nat.eq C c2 (CSort n0))

                      i:nat
                        .getl i (CTail k u1 (CHead c k0 t)) (CHead c2 (Bind b) u2)
                          (or
                               ex2
                                 C
                                 λe:C.eq C c2 (CTail k u1 e)
                                 λe:C.getl i (CHead c k0 t) (CHead e (Bind b) u2)
                               ex4
                                 nat
                                 λ:nat.eq nat i (clen (CHead c k0 t))
                                 λ:nat.eq K k (Bind b)
                                 λ:nat.eq T u1 u2
                                 λn0:nat.eq C c2 (CSort n0))
          we proved 
             i:nat
               .getl i (CTail k u1 c1) (CHead c2 (Bind b) u2)
                 (or
                      ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl i c1 (CHead e (Bind b) u2)
                      ex4
                        nat
                        λ:nat.eq nat i (clen c1)
                        λ:nat.eq K k (Bind b)
                        λ:nat.eq T u1 u2
                        λn:nat.eq C c2 (CSort n))
       we proved 
          k:K
            .b:B
              .u1:T
                .u2:T
                  .c2:C
                    .c1:C
                      .i:nat
                        .getl i (CTail k u1 c1) (CHead c2 (Bind b) u2)
                          (or
                               ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl i c1 (CHead e (Bind b) u2)
                               ex4
                                 nat
                                 λ:nat.eq nat i (clen c1)
                                 λ:nat.eq K k (Bind b)
                                 λ:nat.eq T u1 u2
                                 λn:nat.eq C c2 (CSort n))