DEFINITION getl_gen_2()
TYPE =
       ∀c1:C.∀c2:C.∀i:nat.(getl i c1 c2)→(ex_3 B C T λb:B.λc:C.λv:T.eq C c2 (CHead c (Bind b) v))
BODY =
        assume c1: C
        assume c2: C
        assume i: nat
        suppose H: getl i c1 c2
          (H0) 
             by (getl_gen_all . . . H)
ex2 C λe:C.drop i O c1 e λe:C.clear e c2
          end of H0
          we proceed by induction on H0 to prove ex_3 B C T λb:B.λc:C.λv:T.eq C c2 (CHead c (Bind b) v)
             case ex_intro2 : x:C :drop i O c1 x H2:clear x c2 ⇒
                the thesis becomes ex_3 B C T λb:B.λc:C.λv:T.eq C c2 (CHead c (Bind b) v)
                   (H3) 
                      by (clear_gen_all . . H2)
ex_3 B C T λb:B.λe:C.λu:T.eq C c2 (CHead e (Bind b) u)
                   end of H3
                   we proceed by induction on H3 to prove ex_3 B C T λb:B.λc:C.λv:T.eq C c2 (CHead c (Bind b) v)
                      case ex_3_intro : x0:B x1:C x2:T H4:eq C c2 (CHead x1 (Bind x0) x2) ⇒
                         the thesis becomes ex_3 B C T λb:B.λc0:C.λv:T.eq C c2 (CHead c0 (Bind b) v)
                            by (refl_equal . .)
                            we proved eq C (CHead x1 (Bind x0) x2) (CHead x1 (Bind x0) x2)
                            by (ex_3_intro . . . . . . . previous)
                            we proved ex_3 B C T λb:B.λc:C.λv:T.eq C (CHead x1 (Bind x0) x2) (CHead c (Bind b) v)
                            by (eq_ind_r . . . previous . H4)
ex_3 B C T λb:B.λc0:C.λv:T.eq C c2 (CHead c0 (Bind b) v)
ex_3 B C T λb:B.λc:C.λv:T.eq C c2 (CHead c (Bind b) v)
          we proved ex_3 B C T λb:B.λc:C.λv:T.eq C c2 (CHead c (Bind b) v)
       we proved 
          ∀c1:C.∀c2:C.∀i:nat.(getl i c1 c2)→(ex_3 B C T λb:B.λc:C.λv:T.eq C c2 (CHead c (Bind b) v))