DEFINITION sn3_gen_lift()
TYPE =
       ∀c1:C.∀t:T.∀h:nat.∀d:nat.(sn3 c1 (lift h d t))→∀c2:C.(drop h d c1 c2)→(sn3 c2 t)
BODY =
        assume c1: C
        assume t: T
        assume h: nat
        assume d: nat
        suppose H: sn3 c1 (lift h d t)
           assume y: T
           suppose H0: sn3 c1 y
             we proceed by induction on H0 to prove ∀x:T.(eq T y (lift h d x))→∀c2:C.(drop h d c1 c2)→(sn3 c2 x)
                case sn3_sing : t1:T H1:∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c1 t1 t2)→(sn3 c1 t2) ⇒
                   the thesis becomes ∀x:T.∀H3:(eq T t1 (lift h d x)).∀c2:C.∀H4:(drop h d c1 c2).(sn3 c2 x)
                   (H2) by induction hypothesis we know 
                      ∀t2:T
                        .(eq T t1 t2)→∀P:Prop.P
                          →(pr3 c1 t1 t2)→∀x:T.(eq T t2 (lift h d x))→∀c2:C.(drop h d c1 c2)→(sn3 c2 x)
                       assume x: T
                       suppose H3: eq T t1 (lift h d x)
                       assume c2: C
                       suppose H4: drop h d c1 c2
                         (H5) 
                            we proceed by induction on H3 to prove 
                               ∀t2:T
                                 .(eq T (lift h d x) t2)→∀P:Prop.P
                                   →(pr3 c1 (lift h d x) t2
                                        →∀x0:T.(eq T t2 (lift h d x0))→∀c3:C.(drop h d c1 c3)→(sn3 c3 x0))
                               case refl_equal : ⇒
                                  the thesis becomes the hypothesis H2

                               ∀t2:T
                                 .(eq T (lift h d x) t2)→∀P:Prop.P
                                   →(pr3 c1 (lift h d x) t2
                                        →∀x0:T.(eq T t2 (lift h d x0))→∀c3:C.(drop h d c1 c3)→(sn3 c3 x0))
                         end of H5
                          assume t2: T
                          suppose H7: (eq T x t2)→∀P:Prop.P
                          suppose H8: pr3 c2 x t2
                            (h1) 
                                suppose H9: eq T (lift h d x) (lift h d t2)
                                assume P: Prop
                                  (H11) 
                                     by (lift_inj . . . . H9)
                                     we proved eq T x t2
                                     by (eq_ind_r . . . H7 . previous)
(eq T x x)→∀P0:Prop.P0
                                  end of H11
                                  by (refl_equal . .)
                                  we proved eq T x x
                                  by (H11 previous .)
                                  we proved P
(eq T (lift h d x) (lift h d t2))→∀P:Prop.P
                            end of h1
                            (h2) 
                               by (pr3_lift . . . . H4 . . H8)
pr3 c1 (lift h d x) (lift h d t2)
                            end of h2
                            (h3) 
                               by (refl_equal . .)
eq T (lift h d t2) (lift h d t2)
                            end of h3
                            by (H5 . h1 h2 . h3 . H4)
                            we proved sn3 c2 t2
                         we proved ∀t2:T.((eq T x t2)→∀P:Prop.P)→(pr3 c2 x t2)→(sn3 c2 t2)
                         by (sn3_sing . . previous)
                         we proved sn3 c2 x
∀x:T.∀H3:(eq T t1 (lift h d x)).∀c2:C.∀H4:(drop h d c1 c2).(sn3 c2 x)
             we proved ∀x:T.(eq T y (lift h d x))→∀c2:C.(drop h d c1 c2)→(sn3 c2 x)
             by (unintro . . . previous)
             we proved (eq T y (lift h d t))→∀c2:C.(drop h d c1 c2)→(sn3 c2 t)
          we proved ∀y:T.(sn3 c1 y)→(eq T y (lift h d t))→∀c2:C.(drop h d c1 c2)→(sn3 c2 t)
          by (insert_eq . . . . previous H)
          we proved ∀c2:C.(drop h d c1 c2)→(sn3 c2 t)
       we proved ∀c1:C.∀t:T.∀h:nat.∀d:nat.(sn3 c1 (lift h d t))→∀c2:C.(drop h d c1 c2)→(sn3 c2 t)