DEFINITION drop_conf_rev()
TYPE =
       ∀j:nat
         .∀e1:C
           .∀e2:C
             .drop j O e1 e2
               →∀c2:C.∀i:nat.(drop i O c2 e2)→(ex2 C λc1:C.drop j O c1 c2 λc1:C.drop i j c1 e1)
BODY =
Show proof