DEFINITION drop_clear()
TYPE =
       ∀c1:C
         .∀c2:C
           .∀i:nat
             .drop (S i) O c1 c2
               →ex2_3 B C T λb:B.λe:C.λv:T.clear c1 (CHead e (Bind b) v) λ:B.λe:C.λ:T.drop i O e c2
BODY =
       assume c1: C
          we proceed by induction on c1 to prove 
             ∀c2:C
               .∀i:nat
                 .drop (S i) O c1 c2
                   →ex2_3 B C T λb:B.λe:C.λv:T.clear c1 (CHead e (Bind b) v) λ:B.λe:C.λ:T.drop i O e c2
             case CSort : n:nat ⇒
                the thesis becomes 
                ∀c2:C
                  .∀i:nat
                    .∀H:drop (S i) O (CSort n) c2
                      .ex2_3
                        B
                        C
                        T
                        λb:B.λe:C.λv:T.clear (CSort n) (CHead e (Bind b) v)
                        λ:B.λe:C.λ:T.drop i O e c2
                    assume c2: C
                    assume i: nat
                    suppose H: drop (S i) O (CSort n) c2
                      by (drop_gen_sort . . . . H)
                      we proved and3 (eq C c2 (CSort n)) (eq nat (S i) O) (eq nat O O)
                      we proceed by induction on the previous result to prove 
                         ex2_3
                           B
                           C
                           T
                           λb:B.λe:C.λv:T.clear (CSort n) (CHead e (Bind b) v)
                           λ:B.λe:C.λ:T.drop i O e c2
                         case and3_intro : :eq C c2 (CSort n) H1:eq nat (S i) O :eq nat O O ⇒
                            the thesis becomes 
                            ex2_3
                              B
                              C
                              T
                              λb:B.λe:C.λv:T.clear (CSort n) (CHead e (Bind b) v)
                              λ:B.λe:C.λ:T.drop i O e c2
                               (H3) 
                                  we proceed by induction on H1 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                     case refl_equal : ⇒
                                        the thesis becomes <λ:nat.Prop> CASE S i OF O⇒False | S ⇒True
                                           consider I
                                           we proved True
<λ:nat.Prop> CASE S i OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                               end of H3
                               consider H3
                               we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                               that is equivalent to False
                               we proceed by induction on the previous result to prove 
                                  ex2_3
                                    B
                                    C
                                    T
                                    λb:B.λe:C.λv:T.clear (CSort n) (CHead e (Bind b) v)
                                    λ:B.λe:C.λ:T.drop i O e c2

                                  ex2_3
                                    B
                                    C
                                    T
                                    λb:B.λe:C.λv:T.clear (CSort n) (CHead e (Bind b) v)
                                    λ:B.λe:C.λ:T.drop i O e c2
                      we proved 
                         ex2_3
                           B
                           C
                           T
                           λb:B.λe:C.λv:T.clear (CSort n) (CHead e (Bind b) v)
                           λ:B.λe:C.λ:T.drop i O e c2

                      ∀c2:C
                        .∀i:nat
                          .∀H:drop (S i) O (CSort n) c2
                            .ex2_3
                              B
                              C
                              T
                              λb:B.λe:C.λv:T.clear (CSort n) (CHead e (Bind b) v)
                              λ:B.λe:C.λ:T.drop i O e c2
             case CHead : c:C k:K t:T ⇒
                the thesis becomes 
                ∀c2:C
                  .∀i:nat
                    .∀H0:drop (S i) O (CHead c k t) c2
                      .ex2_3
                        B
                        C
                        T
                        λb:B.λe:C.λv:T.clear (CHead c k t) (CHead e (Bind b) v)
                        λ:B.λe:C.λ:T.drop i O e c2
                (H) by induction hypothesis we know 
                   ∀c2:C
                     .∀i:nat
                       .drop (S i) O c c2
                         →ex2_3 B C T λb:B.λe:C.λv:T.clear c (CHead e (Bind b) v) λ:B.λe:C.λ:T.drop i O e c2
                    assume c2: C
                    assume i: nat
                    suppose H0: drop (S i) O (CHead c k t) c2
                      by (drop_gen_drop . . . . . H0)
                      we proved drop (r k i) O c c2
                         assume b: B
                         suppose H1: drop (r (Bind b) i) O c c2
                            (h1) 
                               by (clear_bind . . .)
clear (CHead c (Bind b) t) (CHead c (Bind b) t)
                            end of h1
                            (h2) 
                               consider H1
                               we proved drop (r (Bind b) i) O c c2
drop i O c c2
                            end of h2
                            by (ex2_3_intro . . . . . . . . h1 h2)
                            we proved 
                               ex2_3
                                 B
                                 C
                                 T
                                 λb0:B.λe:C.λv:T.clear (CHead c (Bind b) t) (CHead e (Bind b0) v)
                                 λ:B.λe:C.λ:T.drop i O e c2

                            ∀H1:drop (r (Bind b) i) O c c2
                              .ex2_3
                                B
                                C
                                T
                                λb0:B.λe:C.λv:T.clear (CHead c (Bind b) t) (CHead e (Bind b0) v)
                                λ:B.λe:C.λ:T.drop i O e c2
                         assume f: F
                         suppose H1: drop (r (Flat f) i) O c c2
                            (H2) 
                               consider H1
                               we proved drop (r (Flat f) i) O c c2
                               that is equivalent to drop (S i) O c c2
                               by (H . . previous)
ex2_3 B C T λb:B.λe:C.λv:T.clear c (CHead e (Bind b) v) λ:B.λe:C.λ:T.drop i O e c2
                            end of H2
                            we proceed by induction on H2 to prove 
                               ex2_3
                                 B
                                 C
                                 T
                                 λb:B.λe:C.λv:T.clear (CHead c (Flat f) t) (CHead e (Bind b) v)
                                 λ:B.λe:C.λ:T.drop i O e c2
                               case ex2_3_intro : x0:B x1:C x2:T H3:clear c (CHead x1 (Bind x0) x2) H4:drop i O x1 c2 ⇒
                                  the thesis becomes 
                                  ex2_3
                                    B
                                    C
                                    T
                                    λb:B.λe:C.λv:T.clear (CHead c (Flat f) t) (CHead e (Bind b) v)
                                    λ:B.λe:C.λ:T.drop i O e c2
                                     by (clear_flat . . H3 . .)
                                     we proved clear (CHead c (Flat f) t) (CHead x1 (Bind x0) x2)
                                     by (ex2_3_intro . . . . . . . . previous H4)

                                        ex2_3
                                          B
                                          C
                                          T
                                          λb:B.λe:C.λv:T.clear (CHead c (Flat f) t) (CHead e (Bind b) v)
                                          λ:B.λe:C.λ:T.drop i O e c2
                            we proved 
                               ex2_3
                                 B
                                 C
                                 T
                                 λb:B.λe:C.λv:T.clear (CHead c (Flat f) t) (CHead e (Bind b) v)
                                 λ:B.λe:C.λ:T.drop i O e c2

                            ∀H1:drop (r (Flat f) i) O c c2
                              .ex2_3
                                B
                                C
                                T
                                λb:B.λe:C.λv:T.clear (CHead c (Flat f) t) (CHead e (Bind b) v)
                                λ:B.λe:C.λ:T.drop i O e c2
                      by (previous . previous)
                      we proved 
                         ex2_3
                           B
                           C
                           T
                           λb:B.λe:C.λv:T.clear (CHead c k t) (CHead e (Bind b) v)
                           λ:B.λe:C.λ:T.drop i O e c2

                      ∀c2:C
                        .∀i:nat
                          .∀H0:drop (S i) O (CHead c k t) c2
                            .ex2_3
                              B
                              C
                              T
                              λb:B.λe:C.λv:T.clear (CHead c k t) (CHead e (Bind b) v)
                              λ:B.λe:C.λ:T.drop i O e c2
          we proved 
             ∀c2:C
               .∀i:nat
                 .drop (S i) O c1 c2
                   →ex2_3 B C T λb:B.λe:C.λv:T.clear c1 (CHead e (Bind b) v) λ:B.λe:C.λ:T.drop i O e c2
       we proved 
          ∀c1:C
            .∀c2:C
              .∀i:nat
                .drop (S i) O c1 c2
                  →ex2_3 B C T λb:B.λe:C.λv:T.clear c1 (CHead e (Bind b) v) λ:B.λe:C.λ:T.drop i O e c2