DEFINITION csubst1_getl_ge_back()
TYPE =
       ∀i:nat
         .∀n:nat.(le i n)→∀c1:C.∀c2:C.∀v:T.(csubst1 i v c1 c2)→∀e:C.(getl n c2 e)→(getl n c1 e)
BODY =
Show proof