DEFINITION subst1_head()
TYPE =
       ∀v:T
         .∀u1:T
           .∀u2:T
             .∀i:nat
               .(subst1 i v u1 u2)→∀k:K.∀t1:T.∀t2:T.(subst1 (s k i) v t1 t2)→(subst1 i v (THead k u1 t1) (THead k u2 t2))
BODY =
        assume v: T
        assume u1: T
        assume u2: T
        assume i: nat
        suppose H: subst1 i v u1 u2
          we proceed by induction on H to prove ∀k:K.∀t1:T.∀t2:T.(subst1 (s k i) v t1 t2)→(subst1 i v (THead k u1 t1) (THead k u2 t2))
             case subst1_refl : ⇒
                the thesis becomes ∀k:K.∀t1:T.∀t2:T.(subst1 (s k i) v t1 t2)→(subst1 i v (THead k u1 t1) (THead k u1 t2))
                    assume k: K
                    assume t1: T
                    assume t2: T
                    suppose H0: subst1 (s k i) v t1 t2
                      we proceed by induction on H0 to prove subst1 i v (THead k u1 t1) (THead k u1 t2)
                         case subst1_refl : ⇒
                            the thesis becomes subst1 i v (THead k u1 t1) (THead k u1 t1)
                               by (subst1_refl . . .)
subst1 i v (THead k u1 t1) (THead k u1 t1)
                         case subst1_single : t3:T H1:subst0 (s k i) v t1 t3 ⇒
                            the thesis becomes subst1 i v (THead k u1 t1) (THead k u1 t3)
                               by (subst0_snd . . . . . H1 .)
                               we proved subst0 i v (THead k u1 t1) (THead k u1 t3)
                               by (subst1_single . . . . previous)
subst1 i v (THead k u1 t1) (THead k u1 t3)
                      we proved subst1 i v (THead k u1 t1) (THead k u1 t2)
∀k:K.∀t1:T.∀t2:T.(subst1 (s k i) v t1 t2)→(subst1 i v (THead k u1 t1) (THead k u1 t2))
             case subst1_single : t2:T H0:subst0 i v u1 t2 ⇒
                the thesis becomes ∀k:K.∀t1:T.∀t0:T.∀H1:(subst1 (s k i) v t1 t0).(subst1 i v (THead k u1 t1) (THead k t2 t0))
                    assume k: K
                    assume t1: T
                    assume t0: T
                    suppose H1: subst1 (s k i) v t1 t0
                      we proceed by induction on H1 to prove subst1 i v (THead k u1 t1) (THead k t2 t0)
                         case subst1_refl : ⇒
                            the thesis becomes subst1 i v (THead k u1 t1) (THead k t2 t1)
                               by (subst0_fst . . . . H0 . .)
                               we proved subst0 i v (THead k u1 t1) (THead k t2 t1)
                               by (subst1_single . . . . previous)
subst1 i v (THead k u1 t1) (THead k t2 t1)
                         case subst1_single : t3:T H2:subst0 (s k i) v t1 t3 ⇒
                            the thesis becomes subst1 i v (THead k u1 t1) (THead k t2 t3)
                               by (subst0_both . . . . H0 . . . H2)
                               we proved subst0 i v (THead k u1 t1) (THead k t2 t3)
                               by (subst1_single . . . . previous)
subst1 i v (THead k u1 t1) (THead k t2 t3)
                      we proved subst1 i v (THead k u1 t1) (THead k t2 t0)
∀k:K.∀t1:T.∀t0:T.∀H1:(subst1 (s k i) v t1 t0).(subst1 i v (THead k u1 t1) (THead k t2 t0))
          we proved ∀k:K.∀t1:T.∀t2:T.(subst1 (s k i) v t1 t2)→(subst1 i v (THead k u1 t1) (THead k u2 t2))
       we proved 
          ∀v:T
            .∀u1:T
              .∀u2:T
                .∀i:nat
                  .(subst1 i v u1 u2)→∀k:K.∀t1:T.∀t2:T.(subst1 (s k i) v t1 t2)→(subst1 i v (THead k u1 t1) (THead k u2 t2))