DEFINITION getl_clear_bind()
TYPE =
       ∀b:B
         .∀c:C
           .∀e1:C
             .∀v:T
               .clear c (CHead e1 (Bind b) v)
                 →∀e2:C.∀n:nat.(getl n e1 e2)→(getl (S n) c e2)
BODY =
        assume b: B
        assume c: C
          we proceed by induction on c to prove 
             ∀e1:C
               .∀v:T
                 .clear c (CHead e1 (Bind b) v)
                   →∀e2:C.∀n:nat.(getl n e1 e2)→(getl (S n) c e2)
             case CSort : n:nat ⇒
                the thesis becomes 
                ∀e1:C
                  .∀v:T
                    .∀H:clear (CSort n) (CHead e1 (Bind b) v)
                      .∀e2:C.∀n0:nat.(getl n0 e1 e2)→(getl (S n0) (CSort n) e2)
                    assume e1: C
                    assume v: T
                    suppose H: clear (CSort n) (CHead e1 (Bind b) v)
                    assume e2: C
                    assume n0: nat
                    suppose : getl n0 e1 e2
                      by (clear_gen_sort . . H .)
                      we proved getl (S n0) (CSort n) e2

                      ∀e1:C
                        .∀v:T
                          .∀H:clear (CSort n) (CHead e1 (Bind b) v)
                            .∀e2:C.∀n0:nat.(getl n0 e1 e2)→(getl (S n0) (CSort n) e2)
             case CHead : c0:C k:K t:T ⇒
                the thesis becomes 
                ∀e1:C
                  .∀v:T
                    .∀H0:clear (CHead c0 k t) (CHead e1 (Bind b) v)
                      .∀e2:C.∀n:nat.∀H1:(getl n e1 e2).(getl (S n) (CHead c0 k t) e2)
                (H) by induction hypothesis we know 
                   ∀e1:C
                     .∀v:T
                       .clear c0 (CHead e1 (Bind b) v)
                         →∀e2:C.∀n:nat.(getl n e1 e2)→(getl (S n) c0 e2)
                    assume e1: C
                    assume v: T
                    suppose H0: clear (CHead c0 k t) (CHead e1 (Bind b) v)
                    assume e2: C
                    assume n: nat
                    suppose H1: getl n e1 e2
                         assume b0: B
                         suppose H2: clear (CHead c0 (Bind b0) t) (CHead e1 (Bind b) v)
                            (H3) 
                               by (clear_gen_bind . . . . H2)
                               we proved eq C (CHead e1 (Bind b) v) (CHead c0 (Bind b0) t)
                               by (f_equal . . . . . previous)
                               we proved 
                                  eq
                                    C
                                    <λ:C.C> CASE CHead e1 (Bind b) v OF CSort ⇒e1 | CHead c1  ⇒c1
                                    <λ:C.C> CASE CHead c0 (Bind b0) t OF CSort ⇒e1 | CHead c1  ⇒c1

                                  eq
                                    C
                                    λe:C.<λ:C.C> CASE e OF CSort ⇒e1 | CHead c1  ⇒c1 (CHead e1 (Bind b) v)
                                    λe:C.<λ:C.C> CASE e OF CSort ⇒e1 | CHead c1  ⇒c1 (CHead c0 (Bind b0) t)
                            end of H3
                            (h1) 
                               (H4) 
                                  by (clear_gen_bind . . . . H2)
                                  we proved eq C (CHead e1 (Bind b) v) (CHead c0 (Bind b0) t)
                                  by (f_equal . . . . . previous)
                                  we proved 
                                     eq
                                       B
                                       <λ:C.B>
                                         CASE CHead e1 (Bind b) v OF
                                           CSort ⇒b
                                         | CHead  k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
                                       <λ:C.B>
                                         CASE CHead c0 (Bind b0) t OF
                                           CSort ⇒b
                                         | CHead  k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b

                                     eq
                                       B
                                       λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead  k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
                                         CHead e1 (Bind b) v
                                       λe:C.<λ:C.B> CASE e OF CSort ⇒b | CHead  k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
                                         CHead c0 (Bind b0) t
                               end of H4
                               (H6) 
                                  consider H4
                                  we proved 
                                     eq
                                       B
                                       <λ:C.B>
                                         CASE CHead e1 (Bind b) v OF
                                           CSort ⇒b
                                         | CHead  k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
                                       <λ:C.B>
                                         CASE CHead c0 (Bind b0) t OF
                                           CSort ⇒b
                                         | CHead  k0 ⇒<λ:K.B> CASE k0 OF Bind b1⇒b1 | Flat ⇒b
eq B b b0
                               end of H6
                               suppose H7: eq C e1 c0
                                  (H8) 
                                     we proceed by induction on H7 to prove getl n c0 e2
                                        case refl_equal : ⇒
                                           the thesis becomes the hypothesis H1
getl n c0 e2
                                  end of H8
                                  we proceed by induction on H6 to prove getl (S n) (CHead c0 (Bind b0) t) e2
                                     case refl_equal : ⇒
                                        the thesis becomes getl (S n) (CHead c0 (Bind b) t) e2
                                           consider H8
                                           we proved getl n c0 e2
                                           that is equivalent to getl (r (Bind b) n) c0 e2
                                           by (getl_head . . . . previous .)
getl (S n) (CHead c0 (Bind b) t) e2
                                  we proved getl (S n) (CHead c0 (Bind b0) t) e2
(eq C e1 c0)→(getl (S n) (CHead c0 (Bind b0) t) e2)
                            end of h1
                            (h2) 
                               consider H3
                               we proved 
                                  eq
                                    C
                                    <λ:C.C> CASE CHead e1 (Bind b) v OF CSort ⇒e1 | CHead c1  ⇒c1
                                    <λ:C.C> CASE CHead c0 (Bind b0) t OF CSort ⇒e1 | CHead c1  ⇒c1
eq C e1 c0
                            end of h2
                            by (h1 h2)
                            we proved getl (S n) (CHead c0 (Bind b0) t) e2

                            ∀H2:clear (CHead c0 (Bind b0) t) (CHead e1 (Bind b) v)
                              .getl (S n) (CHead c0 (Bind b0) t) e2
                         assume f: F
                         suppose H2: clear (CHead c0 (Flat f) t) (CHead e1 (Bind b) v)
                            by (clear_gen_flat . . . . H2)
                            we proved clear c0 (CHead e1 (Bind b) v)
                            by (H . . previous . . H1)
                            we proved getl (S n) c0 e2
                            by (getl_flat . . . previous . .)
                            we proved getl (S n) (CHead c0 (Flat f) t) e2

                            ∀H2:clear (CHead c0 (Flat f) t) (CHead e1 (Bind b) v)
                              .getl (S n) (CHead c0 (Flat f) t) e2
                      by (previous . H0)
                      we proved getl (S n) (CHead c0 k t) e2

                      ∀e1:C
                        .∀v:T
                          .∀H0:clear (CHead c0 k t) (CHead e1 (Bind b) v)
                            .∀e2:C.∀n:nat.∀H1:(getl n e1 e2).(getl (S n) (CHead c0 k t) e2)
          we proved 
             ∀e1:C
               .∀v:T
                 .clear c (CHead e1 (Bind b) v)
                   →∀e2:C.∀n:nat.(getl n e1 e2)→(getl (S n) c e2)
       we proved 
          ∀b:B
            .∀c:C
              .∀e1:C
                .∀v:T
                  .clear c (CHead e1 (Bind b) v)
                    →∀e2:C.∀n:nat.(getl n e1 e2)→(getl (S n) c e2)