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 =
        assume i: nat
        assume v: T
        assume c1: C
        assume P: C→Prop
        suppose H: P c1
        suppose H1: ∀c:C.(csubst0 i v c1 c)→(P c)
        assume c: C
        suppose H2: csubst1 i v c1 c
          by cases on H2 we prove P c
             case csubst1_refl ⇒
                the thesis becomes the hypothesis H
             case csubst1_sing c2:C H3:csubst0 i v c1 c2 ⇒
                the thesis becomes P c2
                by (H1 . H3)
P c2
          we proved P c
       we proved 
          ∀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)