DEFINITION drop1_getl_trans()
TYPE =
       ∀hds:PList
         .∀c1:C
           .∀c2:C
             .drop1 hds c2 c1
               →∀b:B
                    .∀e1:C
                      .∀v:T
                        .∀i:nat
                          .getl i c1 (CHead e1 (Bind b) v)
                            →(ex2
                                 C
                                 λe2:C.drop1 (ptrans hds i) e2 e1
                                 λe2:C.getl (trans hds i) c2 (CHead e2 (Bind b) (lift1 (ptrans hds i) v)))
BODY =
Show proof