DEFINITION clear_getl_trans()
TYPE =
       ∀i:nat.∀c2:C.∀c3:C.(getl i c2 c3)→∀c1:C.(clear c1 c2)→(getl i c1 c3)
BODY =
       assume i: nat
          we proceed by induction on i to prove ∀c2:C.∀c3:C.(getl i c2 c3)→∀c1:C.(clear c1 c2)→(getl i c1 c3)
             case O : ⇒
                the thesis becomes ∀c2:C.∀c3:C.(getl O c2 c3)→∀c1:C.(clear c1 c2)→(getl O c1 c3)
                    assume c2: C
                    assume c3: C
                    suppose H: getl O c2 c3
                    assume c1: C
                    suppose H0: clear c1 c2
                      (h1) 
                         by (drop_refl .)
drop O O c1 c1
                      end of h1
                      (h2) 
                         by (getl_gen_O . . H)
                         we proved clear c2 c3
                         by (clear_trans . . H0 . previous)
clear c1 c3
                      end of h2
                      by (getl_intro . . . . h1 h2)
                      we proved getl O c1 c3
∀c2:C.∀c3:C.(getl O c2 c3)→∀c1:C.(clear c1 c2)→(getl O c1 c3)
             case S : n:nat ⇒
                the thesis becomes ∀c2:C.∀c3:C.(getl (S n) c2 c3)→∀c1:C.(clear c1 c2)→(getl (S n) c1 c3)
                () by induction hypothesis we know ∀c2:C.∀c3:C.(getl n c2 c3)→∀c1:C.(clear c1 c2)→(getl n c1 c3)
                   assume c2: C
                      we proceed by induction on c2 to prove ∀c3:C.(getl (S n) c2 c3)→∀c1:C.(clear c1 c2)→(getl (S n) c1 c3)
                         case CSort : n0:nat ⇒
                            the thesis becomes 
                            ∀c3:C.∀H0:(getl (S n) (CSort n0) c3).∀c1:C.(clear c1 (CSort n0))→(getl (S n) c1 c3)
                                assume c3: C
                                suppose H0: getl (S n) (CSort n0) c3
                                assume c1: C
                                suppose : clear c1 (CSort n0)
                                  by (getl_gen_sort . . . H0 .)
                                  we proved getl (S n) c1 c3

                                  ∀c3:C.∀H0:(getl (S n) (CSort n0) c3).∀c1:C.(clear c1 (CSort n0))→(getl (S n) c1 c3)
                         case CHead : c:C k:K t:T ⇒
                            the thesis becomes 
                            ∀c3:C
                              .∀H1:(getl (S n) (CHead c k t) c3).∀c1:C.∀H2:(clear c1 (CHead c k t)).(getl (S n) c1 c3)
                            () by induction hypothesis we know ∀c3:C.(getl (S n) c c3)→∀c1:C.(clear c1 c)→(getl (S n) c1 c3)
                                assume c3: C
                                suppose H1: getl (S n) (CHead c k t) c3
                                assume c1: C
                                suppose H2: clear c1 (CHead c k t)
                                     assume b: B
                                      suppose H3: getl (S n) (CHead c (Bind b) t) c3
                                      suppose H4: clear c1 (CHead c (Bind b) t)
                                        (H5) 
                                           by (getl_gen_S . . . . . H3)
                                           we proved getl (r (Bind b) n) c c3
                                           by (getl_gen_all . . . previous)
ex2 C λe:C.drop (r (Bind b) n) O c e λe:C.clear e c3
                                        end of H5
                                        consider H5
                                        we proved ex2 C λe:C.drop (r (Bind b) n) O c e λe:C.clear e c3
                                        that is equivalent to ex2 C λe:C.drop n O c e λe:C.clear e c3
                                        we proceed by induction on the previous result to prove getl (S n) c1 c3
                                           case ex_intro2 : x:C H6:drop n O c x H7:clear x c3 ⇒
                                              the thesis becomes getl (S n) c1 c3
                                                 by (drop_clear_O . . . . H4 . . H6)
                                                 we proved drop (S n) O c1 x
                                                 by (getl_intro . . . . previous H7)
getl (S n) c1 c3
                                        we proved getl (S n) c1 c3

                                        ∀H3:getl (S n) (CHead c (Bind b) t) c3
                                          .∀H4:(clear c1 (CHead c (Bind b) t)).(getl (S n) c1 c3)
                                     assume f: F
                                      suppose : getl (S n) (CHead c (Flat f) t) c3
                                      suppose H4: clear c1 (CHead c (Flat f) t)
                                        by (clear_gen_flat_r . . . . H4 .)
                                        we proved getl (S n) c1 c3

                                        getl (S n) (CHead c (Flat f) t) c3
                                          →∀H4:(clear c1 (CHead c (Flat f) t)).(getl (S n) c1 c3)
                                  by (previous . H1 H2)
                                  we proved getl (S n) c1 c3

                                  ∀c3:C
                                    .∀H1:(getl (S n) (CHead c k t) c3).∀c1:C.∀H2:(clear c1 (CHead c k t)).(getl (S n) c1 c3)
                      we proved ∀c3:C.(getl (S n) c2 c3)→∀c1:C.(clear c1 c2)→(getl (S n) c1 c3)
∀c2:C.∀c3:C.(getl (S n) c2 c3)→∀c1:C.(clear c1 c2)→(getl (S n) c1 c3)
          we proved ∀c2:C.∀c3:C.(getl i c2 c3)→∀c1:C.(clear c1 c2)→(getl i c1 c3)
       we proved ∀i:nat.∀c2:C.∀c3:C.(getl i c2 c3)→∀c1:C.(clear c1 c2)→(getl i c1 c3)