DEFINITION csubst0_drop_gt_back()
TYPE =
       ∀n:nat
         .∀i:nat
           .(lt i n)→∀c1:C.∀c2:C.∀v:T.(csubst0 i v c1 c2)→∀e:C.(drop n O c2 e)→(drop n O c1 e)
BODY =
Show proof