DEFINITION csubst0_drop_lt_back()
TYPE =
       ∀n:nat
         .∀i:nat
           .lt n i
             →∀c1:C
                  .∀c2:C
                    .∀v:T
                      .csubst0 i v c1 c2
                        →∀e2:C
                             .drop n O c2 e2
                               →or (drop n O c1 e2) (ex2 C λe1:C.csubst0 (minus i n) v e1 e2 λe1:C.drop n O c1 e1)
BODY =
Show proof