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