DEFINITION drop_getl_trans_lt()
TYPE =
       ∀i:nat
         .∀d:nat
           .lt i d
             →∀c1:C
                  .∀c2:C
                    .∀h:nat
                      .drop h d c1 c2
                        →∀b:B
                             .∀e2:C
                               .∀v:T
                                 .getl i c2 (CHead e2 (Bind b) v)
                                   →(ex2
                                        C
                                        λe1:C.getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))
                                        λe1:C.drop h (minus d (S i)) e1 e2)
BODY =
Show proof