DEFINITION sn3_lift()
TYPE =
       ∀d:C.∀t:T.(sn3 d t)→∀c:C.∀h:nat.∀i:nat.(drop h i c d)→(sn3 c (lift h i t))
BODY =
        assume d: C
        assume t: T
        suppose H: sn3 d t
          we proceed by induction on H to prove ∀c:C.∀h:nat.∀i:nat.(drop h i c d)→(sn3 c (lift h i t))
             case sn3_sing : t1:T :∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 d t1 t2)→(sn3 d t2) ⇒
                the thesis becomes ∀c:C.∀h:nat.∀i:nat.∀H2:(drop h i c d).(sn3 c (lift h i t1))
                (H1) by induction hypothesis we know 
                   ∀t2:T
                     .(eq T t1 t2)→∀P:Prop.P
                       →(pr3 d t1 t2)→∀c:C.∀h:nat.∀i:nat.(drop h i c d)→(sn3 c (lift h i t2))
                    assume c: C
                    assume h: nat
                    assume i: nat
                    suppose H2: drop h i c d
                       assume t2: T
                       suppose H3: (eq T (lift h i t1) t2)→∀P:Prop.P
                       suppose H4: pr2 c (lift h i t1) t2
                         (H5) 
                            by (pr2_gen_lift . . . . . H4 . H2)
ex2 T λt2:T.eq T t2 (lift h i t2) λt2:T.pr2 d t1 t2
                         end of H5
                         we proceed by induction on H5 to prove sn3 c t2
                            case ex_intro2 : x:T H6:eq T t2 (lift h i x) H7:pr2 d t1 x ⇒
                               the thesis becomes sn3 c t2
                                  (H8) 
                                     we proceed by induction on H6 to prove (eq T (lift h i t1) (lift h i x))→∀P:Prop.P
                                        case refl_equal : ⇒
                                           the thesis becomes the hypothesis H3
(eq T (lift h i t1) (lift h i x))→∀P:Prop.P
                                  end of H8
                                  (h1) 
                                      suppose H9: eq T t1 x
                                      assume P: Prop
                                        (H10) 
                                           by (eq_ind_r . . . H8 . H9)
(eq T (lift h i t1) (lift h i t1))→∀P0:Prop.P0
                                        end of H10
                                        by (refl_equal . .)
                                        we proved eq T (lift h i t1) (lift h i t1)
                                        by (H10 previous .)
                                        we proved P
(eq T t1 x)→∀P:Prop.P
                                  end of h1
                                  (h2) by (pr3_pr2 . . . H7) we proved pr3 d t1 x
                                  by (H1 . h1 h2 . . . H2)
                                  we proved sn3 c (lift h i x)
                                  by (eq_ind_r . . . previous . H6)
sn3 c t2
                         we proved sn3 c t2
                      we proved ∀t2:T.((eq T (lift h i t1) t2)→∀P:Prop.P)→(pr2 c (lift h i t1) t2)→(sn3 c t2)
                      by (sn3_pr2_intro . . previous)
                      we proved sn3 c (lift h i t1)
∀c:C.∀h:nat.∀i:nat.∀H2:(drop h i c d).(sn3 c (lift h i t1))
          we proved ∀c:C.∀h:nat.∀i:nat.(drop h i c d)→(sn3 c (lift h i t))
       we proved ∀d:C.∀t:T.(sn3 d t)→∀c:C.∀h:nat.∀i:nat.(drop h i c d)→(sn3 c (lift h i t))