DEFINITION drop_conf_lt()
TYPE =
       ∀k:K
         .∀i:nat
           .∀u:T
             .∀c0:C
               .∀c:C
                 .drop i O c (CHead c0 k 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 (r k d) v)
                                   λv:T.λe0:C.drop i O e (CHead e0 k v)
                                   λ:T.λe0:C.drop h (r k d) c0 e0)
BODY =
Show proof