DEFINITION drop_trans_le()
TYPE =
       ∀i:nat
         .∀d:nat
           .le i d
             →∀c1:C
                  .∀c2:C
                    .∀h:nat
                      .drop h d c1 c2
                        →∀e2:C.(drop i O c2 e2)→(ex2 C λe1:C.drop i O c1 e1 λe1:C.drop h (minus d i) e1 e2)
BODY =
Show proof