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