DEFINITION csubst1_flat()
TYPE =
       ∀f:F
         .∀i:nat
           .∀v:T
             .∀u1:T
               .∀u2:T
                 .subst1 i v u1 u2
                   →∀c1:C.∀c2:C.(csubst1 i v c1 c2)→(csubst1 i v (CHead c1 (Flat f) u1) (CHead c2 (Flat f) u2))
BODY =
        assume f: F
        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 i i
          that is equivalent to eq nat (s (Flat f) i) i
          we proceed by induction on the previous result to prove csubst1 i v (CHead c1 (Flat f) u1) (CHead c2 (Flat f) u2)
             case refl_equal : ⇒
                the thesis becomes csubst1 (s (Flat f) i) v (CHead c1 (Flat f) u1) (CHead c2 (Flat f) u2)
                   by (csubst1_head . . . . . H . . H0)
csubst1 (s (Flat f) i) v (CHead c1 (Flat f) u1) (CHead c2 (Flat f) u2)
          we proved csubst1 i v (CHead c1 (Flat f) u1) (CHead c2 (Flat f) u2)
       we proved 
          ∀f:F
            .∀i:nat
              .∀v:T
                .∀u1:T
                  .∀u2:T
                    .subst1 i v u1 u2
                      →∀c1:C.∀c2:C.(csubst1 i v c1 c2)→(csubst1 i v (CHead c1 (Flat f) u1) (CHead c2 (Flat f) u2))