DEFINITION subst1_gen_head()
TYPE =
       ∀k:K
         .∀v:T
           .∀u1:T
             .∀t1:T
               .∀x:T
                 .∀i:nat
                   .subst1 i v (THead k u1 t1) x
                     →ex3_2 T T λu2:T.λt2:T.eq T x (THead k u2 t2) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt2:T.subst1 (s k i) v t1 t2
BODY =
        assume k: K
        assume v: T
        assume u1: T
        assume t1: T
        assume x: T
        assume i: nat
        suppose H: subst1 i v (THead k u1 t1) x
          we proceed by induction on H to prove ex3_2 T T λu2:T.λt2:T.eq T x (THead k u2 t2) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt2:T.subst1 (s k i) v t1 t2
             case subst1_refl : ⇒
                the thesis becomes ex3_2 T T λu2:T.λt2:T.eq T (THead k u1 t1) (THead k u2 t2) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt2:T.subst1 (s k i) v t1 t2
                   (h1) 
                      by (refl_equal . .)
eq T (THead k u1 t1) (THead k u1 t1)
                   end of h1
                   (h2) 
                      by (subst1_refl . . .)
subst1 i v u1 u1
                   end of h2
                   (h3) 
                      by (subst1_refl . . .)
subst1 (s k i) v t1 t1
                   end of h3
                   by (ex3_2_intro . . . . . . . h1 h2 h3)
ex3_2 T T λu2:T.λt2:T.eq T (THead k u1 t1) (THead k u2 t2) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt2:T.subst1 (s k i) v t1 t2
             case subst1_single : t2:T H0:subst0 i v (THead k u1 t1) t2 ⇒
                the thesis becomes ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
                   by (subst0_gen_head . . . . . . H0)
                   we proved 
                      or3
                        ex2 T λu2:T.eq T t2 (THead k u2 t1) λu2:T.subst0 i v u1 u2
                        ex2 T λt2:T.eq T t2 (THead k u1 t2) λt2:T.subst0 (s k i) v t1 t2
                        ex3_2 T T λu2:T.λt2:T.eq T t2 (THead k u2 t2) λu2:T.λ:T.subst0 i v u1 u2 λ:T.λt2:T.subst0 (s k i) v t1 t2
                   we proceed by induction on the previous result to prove ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
                      case or3_intro0 : H1:ex2 T λu2:T.eq T t2 (THead k u2 t1) λu2:T.subst0 i v u1 u2 ⇒
                         the thesis becomes ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
                            we proceed by induction on H1 to prove ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
                               case ex_intro2 : x0:T H2:eq T t2 (THead k x0 t1) H3:subst0 i v u1 x0 ⇒
                                  the thesis becomes ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
                                     (h1) 
                                        by (subst1_single . . . . H3)
subst1 i v u1 x0
                                     end of h1
                                     (h2) 
                                        by (subst1_refl . . .)
subst1 (s k i) v t1 t1
                                     end of h2
                                     by (ex3_2_intro . . . . . . . H2 h1 h2)
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
                      case or3_intro1 : H1:ex2 T λt3:T.eq T t2 (THead k u1 t3) λt3:T.subst0 (s k i) v t1 t3 ⇒
                         the thesis becomes ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
                            we proceed by induction on H1 to prove ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
                               case ex_intro2 : x0:T H2:eq T t2 (THead k u1 x0) H3:subst0 (s k i) v t1 x0 ⇒
                                  the thesis becomes ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
                                     (h1) 
                                        by (subst1_refl . . .)
subst1 i v u1 u1
                                     end of h1
                                     (h2) 
                                        by (subst1_single . . . . H3)
subst1 (s k i) v t1 x0
                                     end of h2
                                     by (ex3_2_intro . . . . . . . H2 h1 h2)
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
                      case or3_intro2 : H1:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst0 i v u1 u2 λ:T.λt3:T.subst0 (s k i) v t1 t3 ⇒
                         the thesis becomes ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
                            we proceed by induction on H1 to prove ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
                               case ex3_2_intro : x0:T x1:T H2:eq T t2 (THead k x0 x1) H3:subst0 i v u1 x0 H4:subst0 (s k i) v t1 x1 ⇒
                                  the thesis becomes ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
                                     (h1) 
                                        by (subst1_single . . . . H3)
subst1 i v u1 x0
                                     end of h1
                                     (h2) 
                                        by (subst1_single . . . . H4)
subst1 (s k i) v t1 x1
                                     end of h2
                                     by (ex3_2_intro . . . . . . . H2 h1 h2)
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
ex3_2 T T λu2:T.λt3:T.eq T t2 (THead k u2 t3) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt3:T.subst1 (s k i) v t1 t3
          we proved ex3_2 T T λu2:T.λt2:T.eq T x (THead k u2 t2) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt2:T.subst1 (s k i) v t1 t2
       we proved 
          ∀k:K
            .∀v:T
              .∀u1:T
                .∀t1:T
                  .∀x:T
                    .∀i:nat
                      .subst1 i v (THead k u1 t1) x
                        →ex3_2 T T λu2:T.λt2:T.eq T x (THead k u2 t2) λu2:T.λ:T.subst1 i v u1 u2 λ:T.λt2:T.subst1 (s k i) v t1 t2