DEFINITION csubst1_head()
TYPE =
       ∀k:K
         .∀i:nat
           .∀v:T.∀u1:T.∀u2:T.(subst1 i v u1 u2)→∀c1:C.∀c2:C.(csubst1 i v c1 c2)→(csubst1 (s k i) v (CHead c1 k u1) (CHead c2 k u2))
BODY =
        assume k: K
        assume i: nat
        assume v: T
        assume u1: T
        assume u2: T
        suppose H: subst1 i v u1 u2
          we proceed by induction on H to prove ∀c1:C.∀c2:C.(csubst1 i v c1 c2)→(csubst1 (s k i) v (CHead c1 k u1) (CHead c2 k u2))
             case subst1_refl : ⇒
                the thesis becomes ∀c1:C.∀c2:C.(csubst1 i v c1 c2)→(csubst1 (s k i) v (CHead c1 k u1) (CHead c2 k u1))
                    assume c1: C
                    assume c2: C
                    suppose H0: csubst1 i v c1 c2
                      we proceed by induction on H0 to prove csubst1 (s k i) v (CHead c1 k u1) (CHead c2 k u1)
                         case csubst1_refl : ⇒
                            the thesis becomes csubst1 (s k i) v (CHead c1 k u1) (CHead c1 k u1)
                               by (csubst1_refl . . .)
csubst1 (s k i) v (CHead c1 k u1) (CHead c1 k u1)
                         case csubst1_sing : c3:C H1:csubst0 i v c1 c3 ⇒
                            the thesis becomes csubst1 (s k i) v (CHead c1 k u1) (CHead c3 k u1)
                               by (csubst0_fst . . . . . H1 .)
                               we proved csubst0 (s k i) v (CHead c1 k u1) (CHead c3 k u1)
                               by (csubst1_sing . . . . previous)
csubst1 (s k i) v (CHead c1 k u1) (CHead c3 k u1)
                      we proved csubst1 (s k i) v (CHead c1 k u1) (CHead c2 k u1)
∀c1:C.∀c2:C.(csubst1 i v c1 c2)→(csubst1 (s k i) v (CHead c1 k u1) (CHead c2 k u1))
             case subst1_single : t2:T H0:subst0 i v u1 t2 ⇒
                the thesis becomes ∀c1:C.∀c2:C.∀H1:(csubst1 i v c1 c2).(csubst1 (s k i) v (CHead c1 k u1) (CHead c2 k t2))
                    assume c1: C
                    assume c2: C
                    suppose H1: csubst1 i v c1 c2
                      we proceed by induction on H1 to prove csubst1 (s k i) v (CHead c1 k u1) (CHead c2 k t2)
                         case csubst1_refl : ⇒
                            the thesis becomes csubst1 (s k i) v (CHead c1 k u1) (CHead c1 k t2)
                               by (csubst0_snd . . . . . H0 .)
                               we proved csubst0 (s k i) v (CHead c1 k u1) (CHead c1 k t2)
                               by (csubst1_sing . . . . previous)
csubst1 (s k i) v (CHead c1 k u1) (CHead c1 k t2)
                         case csubst1_sing : c3:C H2:csubst0 i v c1 c3 ⇒
                            the thesis becomes csubst1 (s k i) v (CHead c1 k u1) (CHead c3 k t2)
                               by (csubst0_both . . . . . H0 . . H2)
                               we proved csubst0 (s k i) v (CHead c1 k u1) (CHead c3 k t2)
                               by (csubst1_sing . . . . previous)
csubst1 (s k i) v (CHead c1 k u1) (CHead c3 k t2)
                      we proved csubst1 (s k i) v (CHead c1 k u1) (CHead c2 k t2)
∀c1:C.∀c2:C.∀H1:(csubst1 i v c1 c2).(csubst1 (s k i) v (CHead c1 k u1) (CHead c2 k t2))
          we proved ∀c1:C.∀c2:C.(csubst1 i v c1 c2)→(csubst1 (s k i) v (CHead c1 k u1) (CHead c2 k u2))
       we proved 
          ∀k:K
            .∀i:nat
              .∀v:T.∀u1:T.∀u2:T.(subst1 i v u1 u2)→∀c1:C.∀c2:C.(csubst1 i v c1 c2)→(csubst1 (s k i) v (CHead c1 k u1) (CHead c2 k u2))