DEFINITION getl_clear_trans()
TYPE =
       ∀i:nat.∀c1:C.∀c2:C.(getl i c1 c2)→∀c3:C.(clear c2 c3)→(getl i c1 c3)
BODY =
        assume i: nat
        assume c1: C
        assume c2: C
        suppose H: getl i c1 c2
        assume c3: C
        suppose H0: clear c2 c3
          (H1) 
             by (getl_gen_all . . . H)
ex2 C λe:C.drop i O c1 e λe:C.clear e c2
          end of H1
          we proceed by induction on H1 to prove getl i c1 c3
             case ex_intro2 : x:C H2:drop i O c1 x H3:clear x c2 ⇒
                the thesis becomes getl i c1 c3
                   (H4) 
                      by (clear_gen_all . . H3)
ex_3 B C T λb:B.λe:C.λu:T.eq C c2 (CHead e (Bind b) u)
                   end of H4
                   we proceed by induction on H4 to prove getl i c1 c3
                      case ex_3_intro : x0:B x1:C x2:T H5:eq C c2 (CHead x1 (Bind x0) x2) ⇒
                         the thesis becomes getl i c1 c3
                            (H6) 
                               we proceed by induction on H5 to prove clear x (CHead x1 (Bind x0) x2)
                                  case refl_equal : ⇒
                                     the thesis becomes the hypothesis H3
clear x (CHead x1 (Bind x0) x2)
                            end of H6
                            (H7) 
                               we proceed by induction on H5 to prove clear (CHead x1 (Bind x0) x2) c3
                                  case refl_equal : ⇒
                                     the thesis becomes the hypothesis H0
clear (CHead x1 (Bind x0) x2) c3
                            end of H7
                            (h1) 
                               by (getl_intro . . . . H2 H6)
getl i c1 (CHead x1 (Bind x0) x2)
                            end of h1
                            (h2) 
                               by (clear_gen_bind . . . . H7)
eq C c3 (CHead x1 (Bind x0) x2)
                            end of h2
                            by (eq_ind_r . . . h1 . h2)
getl i c1 c3
getl i c1 c3
          we proved getl i c1 c3
       we proved ∀i:nat.∀c1:C.∀c2:C.(getl i c1 c2)→∀c3:C.(clear c2 c3)→(getl i c1 c3)