DEFINITION sty1_lift()
TYPE =
       ∀g:G
         .∀e:C
           .∀t1:T
             .∀t2:T
               .sty1 g e t1 t2
                 →∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sty1 g c (lift h d t1) (lift h d t2))
BODY =
        assume g: G
        assume e: C
        assume t1: T
        assume t2: T
        suppose H: sty1 g e t1 t2
          we proceed by induction on H to prove ∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sty1 g c (lift h d t1) (lift h d t2))
             case sty1_sty0 : t3:T H0:sty0 g e t1 t3 ⇒
                the thesis becomes ∀c:C.∀h:nat.∀d:nat.∀H1:(drop h d c e).(sty1 g c (lift h d t1) (lift h d t3))
                    assume c: C
                    assume h: nat
                    assume d: nat
                    suppose H1: drop h d c e
                      by (sty0_lift . . . . H0 . . . H1)
                      we proved sty0 g c (lift h d t1) (lift h d t3)
                      by (sty1_sty0 . . . . previous)
                      we proved sty1 g c (lift h d t1) (lift h d t3)
∀c:C.∀h:nat.∀d:nat.∀H1:(drop h d c e).(sty1 g c (lift h d t1) (lift h d t3))
             case sty1_sing : t:T :sty1 g e t1 t t3:T H2:sty0 g e t t3 ⇒
                the thesis becomes ∀c:C.∀h:nat.∀d:nat.∀H3:(drop h d c e).(sty1 g c (lift h d t1) (lift h d t3))
                (H1) by induction hypothesis we know ∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sty1 g c (lift h d t1) (lift h d t))
                    assume c: C
                    assume h: nat
                    assume d: nat
                    suppose H3: drop h d c e
                      (h1) 
                         by (H1 . . . H3)
sty1 g c (lift h d t1) (lift h d t)
                      end of h1
                      (h2) 
                         by (sty0_lift . . . . H2 . . . H3)
sty0 g c (lift h d t) (lift h d t3)
                      end of h2
                      by (sty1_sing . . . . h1 . h2)
                      we proved sty1 g c (lift h d t1) (lift h d t3)
∀c:C.∀h:nat.∀d:nat.∀H3:(drop h d c e).(sty1 g c (lift h d t1) (lift h d t3))
          we proved ∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sty1 g c (lift h d t1) (lift h d t2))
       we proved 
          ∀g:G
            .∀e:C
              .∀t1:T
                .∀t2:T
                  .sty1 g e t1 t2
                    →∀c:C.∀h:nat.∀d:nat.(drop h d c e)→(sty1 g c (lift h d t1) (lift h d t2))