DEFINITION csubst0_snd_bind()
TYPE =
       ∀b:B
         .∀i:nat
           .∀v:T
             .∀u1:T
               .∀u2:T
                 .(subst0 i v u1 u2)→∀c:C.(csubst0 (S i) v (CHead c (Bind b) u1) (CHead c (Bind b) u2))
BODY =
        assume b: B
        assume i: nat
        assume v: T
        assume u1: T
        assume u2: T
        suppose H: subst0 i v u1 u2
        assume c: C
          by (refl_equal . .)
          we proved eq nat (S i) (S i)
          that is equivalent to eq nat (s (Bind b) i) (S i)
          we proceed by induction on the previous result to prove csubst0 (S i) v (CHead c (Bind b) u1) (CHead c (Bind b) u2)
             case refl_equal : ⇒
                the thesis becomes csubst0 (s (Bind b) i) v (CHead c (Bind b) u1) (CHead c (Bind b) u2)
                   by (csubst0_snd . . . . . H .)
csubst0 (s (Bind b) i) v (CHead c (Bind b) u1) (CHead c (Bind b) u2)
          we proved csubst0 (S i) v (CHead c (Bind b) u1) (CHead c (Bind b) u2)
       we proved 
          ∀b:B
            .∀i:nat
              .∀v:T
                .∀u1:T
                  .∀u2:T
                    .(subst0 i v u1 u2)→∀c:C.(csubst0 (S i) v (CHead c (Bind b) u1) (CHead c (Bind b) u2))