DEFINITION getl_drop_conf_lt()
TYPE =
       ∀b:B
         .∀c:C
           .∀c0:C
             .∀u:T
               .∀i:nat
                 .getl i c (CHead c0 (Bind b) u)
                   →∀e:C
                        .∀h:nat
                          .∀d:nat
                            .drop h (S (plus i d)) c e
                              →(ex3_2
                                   T
                                   C
                                   λv:T.λ:C.eq T u (lift h d v)
                                   λv:T.λe0:C.getl i e (CHead e0 (Bind b) v)
                                   λ:T.λe0:C.drop h d c0 e0)
BODY =
Show proof