DEFINITION subst1_ex()
TYPE =
       ∀u:T.∀t1:T.∀d:nat.(ex T λt2:T.subst1 d u t1 (lift (S O) d t2))
BODY =
        assume u: T
        assume t1: T
          we proceed by induction on t1 to prove ∀d:nat.(ex T λt2:T.subst1 d u t1 (lift (S O) d t2))
             case TSort : n:nat ⇒
                the thesis becomes ∀d:nat.(ex T λt2:T.subst1 d u (TSort n) (lift (S O) d t2))
                   assume d: nat
                      (h1) 
                         by (subst1_refl . . .)
subst1 d u (TSort n) (TSort n)
                      end of h1
                      (h2) 
                         by (lift_sort . . .)
eq T (lift (S O) d (TSort n)) (TSort n)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved subst1 d u (TSort n) (lift (S O) d (TSort n))
                      by (ex_intro . . . previous)
                      we proved ex T λt2:T.subst1 d u (TSort n) (lift (S O) d t2)
∀d:nat.(ex T λt2:T.subst1 d u (TSort n) (lift (S O) d t2))
             case TLRef : n:nat ⇒
                the thesis becomes ∀d:nat.(ex T λt2:T.subst1 d u (TLRef n) (lift (S O) d t2))
                   assume d: nat
                      (h1) 
                         suppose H: lt n d
                            (h1) 
                               by (subst1_refl . . .)
subst1 d u (TLRef n) (TLRef n)
                            end of h1
                            (h2) 
                               by (lift_lref_lt . . . H)
eq T (lift (S O) d (TLRef n)) (TLRef n)
                            end of h2
                            by (eq_ind_r . . . h1 . h2)
                            we proved subst1 d u (TLRef n) (lift (S O) d (TLRef n))
                            by (ex_intro . . . previous)
                            we proved ex T λt2:T.subst1 d u (TLRef n) (lift (S O) d t2)
(lt n d)→(ex T λt2:T.subst1 d u (TLRef n) (lift (S O) d t2))
                      end of h1
                      (h2) 
                         suppose H: eq nat n d
                            we proceed by induction on H to prove ex T λt2:T.subst1 d u (TLRef n) (lift (S O) d t2)
                               case refl_equal : ⇒
                                  the thesis becomes ex T λt2:T.subst1 n u (TLRef n) (lift (S O) n t2)
                                     (h1) 
                                        by (subst0_lref . .)
                                        we proved subst0 n u (TLRef n) (lift (S n) O u)
                                        by (subst1_single . . . . previous)
                                        we proved subst1 n u (TLRef n) (lift (S n) O u)
subst1 n u (TLRef n) (lift (plus (S O) n) O u)
                                     end of h1
                                     (h2) 
                                        (h1) 
                                           by (le_n .)
                                           we proved le (plus O n) (plus O n)
le n (plus O n)
                                        end of h1
                                        (h2) by (le_O_n .) we proved le O n
                                        by (lift_free . . . . . h1 h2)
eq T (lift (S O) n (lift n O u)) (lift (plus (S O) n) O u)
                                     end of h2
                                     by (eq_ind_r . . . h1 . h2)
                                     we proved subst1 n u (TLRef n) (lift (S O) n (lift n O u))
                                     by (ex_intro . . . previous)
ex T λt2:T.subst1 n u (TLRef n) (lift (S O) n t2)
                            we proved ex T λt2:T.subst1 d u (TLRef n) (lift (S O) d t2)
(eq nat n d)→(ex T λt2:T.subst1 d u (TLRef n) (lift (S O) d t2))
                      end of h2
                      (h3) 
                         suppose H: lt d n
                            (h1) 
                               by (subst1_refl . . .)
subst1 d u (TLRef n) (TLRef n)
                            end of h1
                            (h2) 
                               by (lift_lref_gt . . H)
eq T (lift (S O) d (TLRef (pred n))) (TLRef n)
                            end of h2
                            by (eq_ind_r . . . h1 . h2)
                            we proved subst1 d u (TLRef n) (lift (S O) d (TLRef (pred n)))
                            by (ex_intro . . . previous)
                            we proved ex T λt2:T.subst1 d u (TLRef n) (lift (S O) d t2)
(lt d n)→(ex T λt2:T.subst1 d u (TLRef n) (lift (S O) d t2))
                      end of h3
                      by (lt_eq_gt_e . . . h1 h2 h3)
                      we proved ex T λt2:T.subst1 d u (TLRef n) (lift (S O) d t2)
∀d:nat.(ex T λt2:T.subst1 d u (TLRef n) (lift (S O) d t2))
             case THead : k:K t:T t0:T ⇒
                the thesis becomes ∀d:nat.(ex T λt2:T.subst1 d u (THead k t t0) (lift (S O) d t2))
                (H) by induction hypothesis we know ∀d:nat.(ex T λt2:T.subst1 d u t (lift (S O) d t2))
                (H0) by induction hypothesis we know ∀d:nat.(ex T λt2:T.subst1 d u t0 (lift (S O) d t2))
                   assume d: nat
                      (H_x) 
                         by (H .)
ex T λt2:T.subst1 d u t (lift (S O) d t2)
                      end of H_x
                      (H1) consider H_x
                      we proceed by induction on H1 to prove ex T λt2:T.subst1 d u (THead k t t0) (lift (S O) d t2)
                         case ex_intro : x:T H2:subst1 d u t (lift (S O) d x) ⇒
                            the thesis becomes ex T λt2:T.subst1 d u (THead k t t0) (lift (S O) d t2)
                               (H_x0) 
                                  by (H0 .)
ex T λt2:T.subst1 (s k d) u t0 (lift (S O) (s k d) t2)
                               end of H_x0
                               (H3) consider H_x0
                               we proceed by induction on H3 to prove ex T λt2:T.subst1 d u (THead k t t0) (lift (S O) d t2)
                                  case ex_intro : x0:T H4:subst1 (s k d) u t0 (lift (S O) (s k d) x0) ⇒
                                     the thesis becomes ex T λt2:T.subst1 d u (THead k t t0) (lift (S O) d t2)
                                        (h1) 
                                           by (subst1_head . . . . H2 . . . H4)

                                              subst1
                                                d
                                                u
                                                THead k t t0
                                                THead k (lift (S O) d x) (lift (S O) (s k d) x0)
                                        end of h1
                                        (h2) 
                                           by (lift_head . . . . .)

                                              eq
                                                T
                                                lift (S O) d (THead k x x0)
                                                THead k (lift (S O) d x) (lift (S O) (s k d) x0)
                                        end of h2
                                        by (eq_ind_r . . . h1 . h2)
                                        we proved subst1 d u (THead k t t0) (lift (S O) d (THead k x x0))
                                        by (ex_intro . . . previous)
ex T λt2:T.subst1 d u (THead k t t0) (lift (S O) d t2)
ex T λt2:T.subst1 d u (THead k t t0) (lift (S O) d t2)
                      we proved ex T λt2:T.subst1 d u (THead k t t0) (lift (S O) d t2)
∀d:nat.(ex T λt2:T.subst1 d u (THead k t t0) (lift (S O) d t2))
          we proved ∀d:nat.(ex T λt2:T.subst1 d u t1 (lift (S O) d t2))
       we proved ∀u:T.∀t1:T.∀d:nat.(ex T λt2:T.subst1 d u t1 (lift (S O) d t2))