DEFINITION drop_gen_refl()
TYPE =
       ∀x:C.∀e:C.(drop O O x e)→(eq C x e)
BODY =
        assume x: C
        assume e: C
        suppose H: drop O O x e
           assume y: nat
           suppose H0: drop y O x e
              assume y0: nat
              suppose H1: drop y y0 x e
                we proceed by induction on H1 to prove (eq nat y0 O)→(eq nat y y0)→(eq C x e)
                   case drop_refl : c:C ⇒
                      the thesis becomes (eq nat O O)→(eq nat O O)→(eq C c c)
                          suppose : eq nat O O
                          suppose : eq nat O O
                            by (refl_equal . .)
                            we proved eq C c c
(eq nat O O)→(eq nat O O)→(eq C c c)
                   case drop_drop : k:K h:nat c:C e0:C :drop (r k h) O c e0 u:T ⇒
                      the thesis becomes (eq nat O O)→∀H5:(eq nat (S h) O).(eq C (CHead c k u) e0)
                      () by induction hypothesis we know (eq nat O O)→(eq nat (r k h) O)→(eq C c e0)
                          suppose : eq nat O O
                          suppose H5: eq nat (S h) O
                            (H6) 
                               we proceed by induction on H5 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                  case refl_equal : ⇒
                                     the thesis becomes <λ:nat.Prop> CASE S h OF O⇒False | S ⇒True
                                        consider I
                                        we proved True
<λ:nat.Prop> CASE S h OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                            end of H6
                            consider H6
                            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 eq C (CHead c k u) e0
                            we proved eq C (CHead c k u) e0
(eq nat O O)→∀H5:(eq nat (S h) O).(eq C (CHead c k u) e0)
                   case drop_skip : k:K h:nat d:nat c:C e0:C H2:drop h (r k d) c e0 u:T ⇒
                      the thesis becomes 
                      ∀H4:eq nat (S d) O
                        .∀H5:(eq nat h (S d)).(eq C (CHead c k (lift h (r k d) u)) (CHead e0 k u))
                      (H3) by induction hypothesis we know (eq nat (r k d) O)→(eq nat h (r k d))→(eq C c e0)
                          suppose H4: eq nat (S d) O
                          suppose H5: eq nat h (S d)
                            (H6) 
                               by (f_equal . . . . . H5)
                               we proved eq nat h (S d)
eq nat (λe1:nat.e1 h) (λe1:nat.e1 (S d))
                            end of H6
                            (H9) 
                               we proceed by induction on H4 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                                  case refl_equal : ⇒
                                     the thesis becomes <λ:nat.Prop> CASE S d OF O⇒False | S ⇒True
                                        consider I
                                        we proved True
<λ:nat.Prop> CASE S d OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
                            end of H9
                            consider H9
                            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 eq C (CHead c k (lift (S d) (r k d) u)) (CHead e0 k u)
                            we proved eq C (CHead c k (lift (S d) (r k d) u)) (CHead e0 k u)
                            by (eq_ind_r . . . previous . H6)
                            we proved eq C (CHead c k (lift h (r k d) u)) (CHead e0 k u)

                            ∀H4:eq nat (S d) O
                              .∀H5:(eq nat h (S d)).(eq C (CHead c k (lift h (r k d) u)) (CHead e0 k u))
                we proved (eq nat y0 O)→(eq nat y y0)→(eq C x e)
             we proved ∀y0:nat.(drop y y0 x e)→(eq nat y0 O)→(eq nat y y0)→(eq C x e)
             by (insert_eq . . . . previous H0)
             we proved (eq nat y O)→(eq C x e)
          we proved ∀y:nat.(drop y O x e)→(eq nat y O)→(eq C x e)
          by (insert_eq . . . . previous H)
          we proved eq C x e
       we proved ∀x:C.∀e:C.(drop O O x e)→(eq C x e)