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