DEFINITION drop_clear_S()
TYPE =
       ∀x2:C
         .∀x1:C
           .∀h:nat
             .∀d:nat
               .drop h (S d) x1 x2
                 →∀b:B
                      .∀c2:C
                        .∀u:T
                          .clear x2 (CHead c2 (Bind b) u)
                            →ex2 C λc1:C.clear x1 (CHead c1 (Bind b) (lift h d u)) λc1:C.drop h d c1 c2
BODY =
Show proof