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 =
Show proof