DEFINITION drop_getl_trans_le()
TYPE =
       ∀i:nat
         .∀d:nat
           .le i d
             →∀c1:C
                  .∀c2:C
                    .∀h:nat
                      .drop h d c1 c2
                        →∀e2:C
                             .getl i c2 e2
                               →ex3_2 C C λe0:C.λ:C.drop i O c1 e0 λe0:C.λe1:C.drop h (minus d i) e0 e1 λ:C.λe1:C.clear e1 e2
BODY =
Show proof