DEFINITION getl_gen_bind()
TYPE =
       ∀b:B
         .∀e:C
           .∀d:C
             .∀v:T
               .∀i:nat
                 .getl i (CHead e (Bind b) v) d
                   →(or
                        land (eq nat i O) (eq C d (CHead e (Bind b) v))
                        ex2 nat λj:nat.eq nat i (S j) λj:nat.getl j e d)
BODY =
        assume b: B
        assume e: C
        assume d: C
        assume v: T
        assume i: nat
          we proceed by induction on i to prove 
             getl i (CHead e (Bind b) v) d
               →(or
                    land (eq nat i O) (eq C d (CHead e (Bind b) v))
                    ex2 nat λj:nat.eq nat i (S j) λj:nat.getl j e d)
             case O : ⇒
                the thesis becomes 
                getl O (CHead e (Bind b) v) d
                  →(or
                       land (eq nat O O) (eq C d (CHead e (Bind b) v))
                       ex2 nat λj:nat.eq nat O (S j) λj:nat.getl j e d)
                   suppose H: getl O (CHead e (Bind b) v) d
                      (h1) 
                         (h1) 
                            by (refl_equal . .)
eq nat O O
                         end of h1
                         (h2) 
                            by (refl_equal . .)
eq C (CHead e (Bind b) v) (CHead e (Bind b) v)
                         end of h2
                         by (conj . . h1 h2)
                         we proved 
                            land
                              eq nat O O
                              eq C (CHead e (Bind b) v) (CHead e (Bind b) v)
                         by (or_introl . . previous)

                            or
                              land
                                eq nat O O
                                eq C (CHead e (Bind b) v) (CHead e (Bind b) v)
                              ex2 nat λj:nat.eq nat O (S j) λj:nat.getl j e (CHead e (Bind b) v)
                      end of h1
                      (h2) 
                         by (getl_gen_O . . H)
                         we proved clear (CHead e (Bind b) v) d
                         by (clear_gen_bind . . . . previous)
eq C d (CHead e (Bind b) v)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved 
                         or
                           land (eq nat O O) (eq C d (CHead e (Bind b) v))
                           ex2 nat λj:nat.eq nat O (S j) λj:nat.getl j e d

                      getl O (CHead e (Bind b) v) d
                        →(or
                             land (eq nat O O) (eq C d (CHead e (Bind b) v))
                             ex2 nat λj:nat.eq nat O (S j) λj:nat.getl j e d)
             case S : n:nat ⇒
                the thesis becomes 
                ∀H0:getl (S n) (CHead e (Bind b) v) d
                  .or
                    land (eq nat (S n) O) (eq C d (CHead e (Bind b) v))
                    ex2 nat λj:nat.eq nat (S n) (S j) λj:nat.getl j e d
                () by induction hypothesis we know 
                   getl n (CHead e (Bind b) v) d
                     →(or
                          land (eq nat n O) (eq C d (CHead e (Bind b) v))
                          ex2 nat λj:nat.eq nat n (S j) λj:nat.getl j e d)
                   suppose H0: getl (S n) (CHead e (Bind b) v) d
                      (h1) 
                         by (refl_equal . .)
eq nat (S n) (S n)
                      end of h1
                      (h2) 
                         by (getl_gen_S . . . . . H0)
                         we proved getl (r (Bind b) n) e d
getl n e d
                      end of h2
                      by (ex_intro2 . . . . h1 h2)
                      we proved ex2 nat λj:nat.eq nat (S n) (S j) λj:nat.getl j e d
                      by (or_intror . . previous)
                      we proved 
                         or
                           land (eq nat (S n) O) (eq C d (CHead e (Bind b) v))
                           ex2 nat λj:nat.eq nat (S n) (S j) λj:nat.getl j e d

                      ∀H0:getl (S n) (CHead e (Bind b) v) d
                        .or
                          land (eq nat (S n) O) (eq C d (CHead e (Bind b) v))
                          ex2 nat λj:nat.eq nat (S n) (S j) λj:nat.getl j e d
          we proved 
             getl i (CHead e (Bind b) v) d
               →(or
                    land (eq nat i O) (eq C d (CHead e (Bind b) v))
                    ex2 nat λj:nat.eq nat i (S j) λj:nat.getl j e d)
       we proved 
          ∀b:B
            .∀e:C
              .∀d:C
                .∀v:T
                  .∀i:nat
                    .getl i (CHead e (Bind b) v) d
                      →(or
                           land (eq nat i O) (eq C d (CHead e (Bind b) v))
                           ex2 nat λj:nat.eq nat i (S j) λj:nat.getl j e d)