DEFINITION subst_subst0()
TYPE =
       ∀v:T.∀t1:T.∀t2:T.∀d:nat.(subst0 d v t1 t2)→(eq T (subst d v t1) (subst d v t2))
BODY =
        assume v: T
        assume t1: T
        assume t2: T
        assume d: nat
        suppose H: subst0 d v t1 t2
          we proceed by induction on H to prove eq T (subst d v t1) (subst d v t2)
             case subst0_lref : v0:T i:nat ⇒
                the thesis becomes eq T (subst i v0 (TLRef i)) (subst i v0 (lift (S i) O v0))
                   (h1) 
                      by (refl_equal . .)
                      we proved eq nat (S i) (S i)
                      that is equivalent to eq nat (plus (S O) i) (S i)
                      we proceed by induction on the previous result to prove eq T (lift i O v0) (subst i v0 (lift (S i) O v0))
                         case refl_equal : ⇒
                            the thesis becomes eq T (lift i O v0) (subst i v0 (lift (plus (S O) i) O v0))
                               (h1) 
                                  by (le_n .)
                                  we proved le (plus O i) (plus O i)
le i (plus O i)
                               end of h1
                               (h2) by (le_O_n .) we proved le O i
                               by (lift_free . . . . . h1 h2)
                               we proved eq T (lift (S O) i (lift i O v0)) (lift (plus (S O) i) O v0)
                               we proceed by induction on the previous result to prove eq T (lift i O v0) (subst i v0 (lift (plus (S O) i) O v0))
                                  case refl_equal : ⇒
                                     the thesis becomes eq T (lift i O v0) (subst i v0 (lift (S O) i (lift i O v0)))
                                        (h1) 
                                           by (refl_equal . .)
eq T (lift i O v0) (lift i O v0)
                                        end of h1
                                        (h2) 
                                           by (subst_lift_SO . . .)
eq T (subst i v0 (lift (S O) i (lift i O v0))) (lift i O v0)
                                        end of h2
                                        by (eq_ind_r . . . h1 . h2)
eq T (lift i O v0) (subst i v0 (lift (S O) i (lift i O v0)))
eq T (lift i O v0) (subst i v0 (lift (plus (S O) i) O v0))
eq T (lift i O v0) (subst i v0 (lift (S i) O v0))
                   end of h1
                   (h2) 
                      by (subst_lref_eq . .)
eq T (subst i v0 (TLRef i)) (lift i O v0)
                   end of h2
                   by (eq_ind_r . . . h1 . h2)
eq T (subst i v0 (TLRef i)) (subst i v0 (lift (S i) O v0))
             case subst0_fst : v0:T u2:T u1:T i:nat :subst0 i v0 u1 u2 t:T k:K ⇒
                the thesis becomes eq T (subst i v0 (THead k u1 t)) (subst i v0 (THead k u2 t))
                (H1) by induction hypothesis we know eq T (subst i v0 u1) (subst i v0 u2)
                   (h1) 
                      (h1) 
                         by (refl_equal . .)
                         we proved 
                            eq
                              T
                              THead k (subst i v0 u2) (subst (s k i) v0 t)
                              THead k (subst i v0 u2) (subst (s k i) v0 t)
                         by (eq_ind_r . . . previous . H1)

                            eq
                              T
                              THead k (subst i v0 u1) (subst (s k i) v0 t)
                              THead k (subst i v0 u2) (subst (s k i) v0 t)
                      end of h1
                      (h2) 
                         by (subst_head . . . . .)

                            eq
                              T
                              subst i v0 (THead k u2 t)
                              THead k (subst i v0 u2) (subst (s k i) v0 t)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)

                         eq
                           T
                           THead k (subst i v0 u1) (subst (s k i) v0 t)
                           subst i v0 (THead k u2 t)
                   end of h1
                   (h2) 
                      by (subst_head . . . . .)

                         eq
                           T
                           subst i v0 (THead k u1 t)
                           THead k (subst i v0 u1) (subst (s k i) v0 t)
                   end of h2
                   by (eq_ind_r . . . h1 . h2)
eq T (subst i v0 (THead k u1 t)) (subst i v0 (THead k u2 t))
             case subst0_snd : k:K v0:T t3:T t4:T i:nat :subst0 (s k i) v0 t4 t3 u:T ⇒
                the thesis becomes eq T (subst i v0 (THead k u t4)) (subst i v0 (THead k u t3))
                (H1) by induction hypothesis we know eq T (subst (s k i) v0 t4) (subst (s k i) v0 t3)
                   (h1) 
                      (h1) 
                         by (refl_equal . .)
                         we proved 
                            eq
                              T
                              THead k (subst i v0 u) (subst (s k i) v0 t3)
                              THead k (subst i v0 u) (subst (s k i) v0 t3)
                         by (eq_ind_r . . . previous . H1)

                            eq
                              T
                              THead k (subst i v0 u) (subst (s k i) v0 t4)
                              THead k (subst i v0 u) (subst (s k i) v0 t3)
                      end of h1
                      (h2) 
                         by (subst_head . . . . .)

                            eq
                              T
                              subst i v0 (THead k u t3)
                              THead k (subst i v0 u) (subst (s k i) v0 t3)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)

                         eq
                           T
                           THead k (subst i v0 u) (subst (s k i) v0 t4)
                           subst i v0 (THead k u t3)
                   end of h1
                   (h2) 
                      by (subst_head . . . . .)

                         eq
                           T
                           subst i v0 (THead k u t4)
                           THead k (subst i v0 u) (subst (s k i) v0 t4)
                   end of h2
                   by (eq_ind_r . . . h1 . h2)
eq T (subst i v0 (THead k u t4)) (subst i v0 (THead k u t3))
             case subst0_both : v0:T u1:T u2:T i:nat :subst0 i v0 u1 u2 k:K t3:T t4:T :subst0 (s k i) v0 t3 t4 ⇒
                the thesis becomes eq T (subst i v0 (THead k u1 t3)) (subst i v0 (THead k u2 t4))
                (H1) by induction hypothesis we know eq T (subst i v0 u1) (subst i v0 u2)
                (H3) by induction hypothesis we know eq T (subst (s k i) v0 t3) (subst (s k i) v0 t4)
                   (h1) 
                      (h1) 
                         by (refl_equal . .)
                         we proved 
                            eq
                              T
                              THead k (subst i v0 u2) (subst (s k i) v0 t4)
                              THead k (subst i v0 u2) (subst (s k i) v0 t4)
                         by (eq_ind_r . . . previous . H3)
                         we proved 
                            eq
                              T
                              THead k (subst i v0 u2) (subst (s k i) v0 t3)
                              THead k (subst i v0 u2) (subst (s k i) v0 t4)
                         by (eq_ind_r . . . previous . H1)

                            eq
                              T
                              THead k (subst i v0 u1) (subst (s k i) v0 t3)
                              THead k (subst i v0 u2) (subst (s k i) v0 t4)
                      end of h1
                      (h2) 
                         by (subst_head . . . . .)

                            eq
                              T
                              subst i v0 (THead k u2 t4)
                              THead k (subst i v0 u2) (subst (s k i) v0 t4)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)

                         eq
                           T
                           THead k (subst i v0 u1) (subst (s k i) v0 t3)
                           subst i v0 (THead k u2 t4)
                   end of h1
                   (h2) 
                      by (subst_head . . . . .)

                         eq
                           T
                           subst i v0 (THead k u1 t3)
                           THead k (subst i v0 u1) (subst (s k i) v0 t3)
                   end of h2
                   by (eq_ind_r . . . h1 . h2)
eq T (subst i v0 (THead k u1 t3)) (subst i v0 (THead k u2 t4))
          we proved eq T (subst d v t1) (subst d v t2)
       we proved ∀v:T.∀t1:T.∀t2:T.∀d:nat.(subst0 d v t1 t2)→(eq T (subst d v t1) (subst d v t2))