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