DEFINITION csubst0_both_bind()
TYPE =
       ∀b:B
         .∀i:nat
           .∀v:T
             .∀u1:T
               .∀u2:T
                 .subst0 i v u1 u2
                   →∀c1:C.∀c2:C.(csubst0 i v c1 c2)→(csubst0 (S i) v (CHead c1 (Bind b) u1) (CHead c2 (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 c1: C
        assume c2: C
        suppose H0: csubst0 i v c1 c2
          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 c1 (Bind b) u1) (CHead c2 (Bind b) u2)
             case refl_equal : ⇒
                the thesis becomes csubst0 (s (Bind b) i) v (CHead c1 (Bind b) u1) (CHead c2 (Bind b) u2)
                   by (csubst0_both . . . . . H . . H0)
csubst0 (s (Bind b) i) v (CHead c1 (Bind b) u1) (CHead c2 (Bind b) u2)
          we proved csubst0 (S i) v (CHead c1 (Bind b) u1) (CHead c2 (Bind b) u2)
       we proved 
          ∀b:B
            .∀i:nat
              .∀v:T
                .∀u1:T
                  .∀u2:T
                    .subst0 i v u1 u2
                      →∀c1:C.∀c2:C.(csubst0 i v c1 c2)→(csubst0 (S i) v (CHead c1 (Bind b) u1) (CHead c2 (Bind b) u2))