DEFINITION csubst1_ind()
TYPE =
       ∀i:nat
         .∀v:T
           .∀c1:C
             .∀P:C→Prop
               .(P c1)→(∀c:C.(csubst0 i v c1 c)→(P c))→∀c:C.(csubst1 i v c1 c)→(P c)
BODY =
Show proof