DEFINITION drop_getl_trans_lt()
TYPE =
       ∀i:nat
         .∀d:nat
           .lt i d
             →∀c1:C
                  .∀c2:C
                    .∀h:nat
                      .drop h d c1 c2
                        →∀b:B
                             .∀e2:C
                               .∀v:T
                                 .getl i c2 (CHead e2 (Bind b) v)
                                   →(ex2
                                        C
                                        λe1:C.getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))
                                        λe1:C.drop h (minus d (S i)) e1 e2)
BODY =
        assume i: nat
        assume d: nat
        suppose H: lt i d
        assume c1: C
        assume c2: C
        assume h: nat
        suppose H0: drop h d c1 c2
        assume b: B
        assume e2: C
        assume v: T
        suppose H1: getl i c2 (CHead e2 (Bind b) v)
          (H2) 
             by (getl_gen_all . . . H1)
ex2 C λe:C.drop i O c2 e λe:C.clear e (CHead e2 (Bind b) v)
          end of H2
          we proceed by induction on H2 to prove 
             ex2
               C
               λe1:C.getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))
               λe1:C.drop h (minus d (S i)) e1 e2
             case ex_intro2 : x:C H3:drop i O c2 x H4:clear x (CHead e2 (Bind b) v) ⇒
                the thesis becomes 
                ex2
                  C
                  λe1:C.getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))
                  λe1:C.drop h (minus d (S i)) e1 e2
                   consider H
                   we proved lt i d
                   that is equivalent to le (S i) d
                   by (le_S . . previous)
                   we proved le (S i) (S d)
                   by (le_S_n . . previous)
                   we proved le i d
                   by (drop_trans_le . . previous . . . H0 . H3)
                   we proved ex2 C λe1:C.drop i O c1 e1 λe1:C.drop h (minus d i) e1 x
                   we proceed by induction on the previous result to prove 
                      ex2
                        C
                        λe1:C.getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))
                        λe1:C.drop h (minus d (S i)) e1 e2
                      case ex_intro2 : x0:C H5:drop i O c1 x0 H6:drop h (minus d i) x0 x ⇒
                         the thesis becomes 
                         ex2
                           C
                           λe1:C.getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))
                           λe1:C.drop h (minus d (S i)) e1 e2
                            (H7) 
                               by (minus_x_Sy . . H)
                               we proved eq nat (minus d i) (S (minus d (S i)))
                               we proceed by induction on the previous result to prove drop h (S (minus d (S i))) x0 x
                                  case refl_equal : ⇒
                                     the thesis becomes the hypothesis H6
drop h (S (minus d (S i))) x0 x
                            end of H7
                            (H8) 
                               by (drop_clear_S . . . . H7 . . . H4)

                                  ex2
                                    C
                                    λc1:C.clear x0 (CHead c1 (Bind b) (lift h (minus d (S i)) v))
                                    λc1:C.drop h (minus d (S i)) c1 e2
                            end of H8
                            we proceed by induction on H8 to prove 
                               ex2
                                 C
                                 λe1:C.getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))
                                 λe1:C.drop h (minus d (S i)) e1 e2
                               case ex_intro2 : x1:C H9:clear x0 (CHead x1 (Bind b) (lift h (minus d (S i)) v)) H10:drop h (minus d (S i)) x1 e2 ⇒
                                  the thesis becomes 
                                  ex2
                                    C
                                    λe1:C.getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))
                                    λe1:C.drop h (minus d (S i)) e1 e2
                                     by (getl_intro . . . . H5 H9)
                                     we proved getl i c1 (CHead x1 (Bind b) (lift h (minus d (S i)) v))
                                     by (ex_intro2 . . . . previous H10)

                                        ex2
                                          C
                                          λe1:C.getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))
                                          λe1:C.drop h (minus d (S i)) e1 e2

                               ex2
                                 C
                                 λe1:C.getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))
                                 λe1:C.drop h (minus d (S i)) e1 e2

                      ex2
                        C
                        λe1:C.getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))
                        λe1:C.drop h (minus d (S i)) e1 e2
          we proved 
             ex2
               C
               λe1:C.getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))
               λe1:C.drop h (minus d (S i)) e1 e2
       we proved 
          ∀i:nat
            .∀d:nat
              .lt i d
                →∀c1:C
                     .∀c2:C
                       .∀h:nat
                         .drop h d c1 c2
                           →∀b:B
                                .∀e2:C
                                  .∀v:T
                                    .getl i c2 (CHead e2 (Bind b) v)
                                      →(ex2
                                           C
                                           λe1:C.getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))
                                           λe1:C.drop h (minus d (S i)) e1 e2)