DEFINITION getl_drop_conf_rev()
TYPE =
       ∀j:nat
         .∀e1:C
           .∀e2:C
             .drop j O e1 e2
               →∀b:B
                    .∀c2:C
                      .∀v2:T
                        .∀i:nat
                          .getl i c2 (CHead e2 (Bind b) v2)
                            →ex2 C λc1:C.drop j O c1 c2 λc1:C.drop (S i) j c1 e1
BODY =
Show proof