DEFINITION getl_conf_ge_drop()
TYPE =
       ∀b:B
         .∀c1:C
           .∀e:C
             .∀u:T
               .∀i:nat
                 .getl i c1 (CHead e (Bind b) u)
                   →∀c2:C.(drop (S O) i c1 c2)→(drop i O c2 e)
BODY =
        assume b: B
        assume c1: C
        assume e: C
        assume u: T
        assume i: nat
        suppose H: getl i c1 (CHead e (Bind b) u)
        assume c2: C
        suppose H0: drop (S O) i c1 c2
          (H3) 
             by (minus_Sx_SO .)
             we proved eq nat (minus (S i) (S O)) i
             we proceed by induction on the previous result to prove drop i O c2 e
                case refl_equal : ⇒
                   the thesis becomes drop (minus (S i) (S O)) O c2 e
                      (h1) 
                         by (getl_drop . . . . . H)
drop (S i) O c1 e
                      end of h1
                      (h2) 
                         (h1) 
                            by (le_n .)
                            we proved le (S i) (S i)
le (plus (S O) i) (S i)
                         end of h1
                         (h2) 
                            by (plus_sym . .)
eq nat (plus i (S O)) (plus (S O) i)
                         end of h2
                         by (eq_ind_r . . . h1 . h2)
le (plus i (S O)) (S i)
                      end of h2
                      by (drop_conf_ge . . . h1 . . . H0 h2)
drop (minus (S i) (S O)) O c2 e
drop i O c2 e
          end of H3
          consider H3
          we proved drop i O c2 e
       we proved 
          ∀b:B
            .∀c1:C
              .∀e:C
                .∀u:T
                  .∀i:nat
                    .getl i c1 (CHead e (Bind b) u)
                      →∀c2:C.(drop (S O) i c1 c2)→(drop i O c2 e)