DEFINITION sns3_lifts()
TYPE =
       ∀c:C
         .∀d:C
           .∀h:nat
             .∀i:nat.(drop h i c d)→∀ts:TList.(sns3 d ts)→(sns3 c (lifts h i ts))
BODY =
        assume c: C
        assume d: C
        assume h: nat
        assume i: nat
        suppose H: drop h i c d
        assume ts: TList
          we proceed by induction on ts to prove (sns3 d ts)→(sns3 c (lifts h i ts))
             case TNil : ⇒
                the thesis becomes (sns3 d TNil)→(sns3 c (lifts h i TNil))
                   we must prove (sns3 d TNil)→(sns3 c (lifts h i TNil))
                   or equivalently True→(sns3 c (lifts h i TNil))
                   suppose H0: True
                      consider H0
                      we proved True
                      that is equivalent to sns3 c (lifts h i TNil)
                   we proved True→(sns3 c (lifts h i TNil))
(sns3 d TNil)→(sns3 c (lifts h i TNil))
             case TCons : t:T t0:TList ⇒
                the thesis becomes (sns3 d (TCons t t0))→(sns3 c (lifts h i (TCons t t0)))
                (H0) by induction hypothesis we know (sns3 d t0)→(sns3 c (lifts h i t0))
                   we must prove (sns3 d (TCons t t0))→(sns3 c (lifts h i (TCons t t0)))
                   or equivalently (land (sn3 d t) (sns3 d t0))→(sns3 c (lifts h i (TCons t t0)))
                   suppose H1: land (sn3 d t) (sns3 d t0)
                      (H2) consider H1
                      we proceed by induction on H2 to prove land (sn3 c (lift h i t)) (sns3 c (lifts h i t0))
                         case conj : H3:sn3 d t H4:sns3 d t0 ⇒
                            the thesis becomes land (sn3 c (lift h i t)) (sns3 c (lifts h i t0))
                               (h1) 
                                  by (sn3_lift . . H3 . . . H)
sn3 c (lift h i t)
                               end of h1
                               (h2) by (H0 H4) we proved sns3 c (lifts h i t0)
                               by (conj . . h1 h2)
land (sn3 c (lift h i t)) (sns3 c (lifts h i t0))
                      we proved land (sn3 c (lift h i t)) (sns3 c (lifts h i t0))
                      that is equivalent to sns3 c (lifts h i (TCons t t0))
                   we proved (land (sn3 d t) (sns3 d t0))→(sns3 c (lifts h i (TCons t t0)))
(sns3 d (TCons t t0))→(sns3 c (lifts h i (TCons t t0)))
          we proved (sns3 d ts)→(sns3 c (lifts h i ts))
       we proved 
          ∀c:C
            .∀d:C
              .∀h:nat
                .∀i:nat.(drop h i c d)→∀ts:TList.(sns3 d ts)→(sns3 c (lifts h i ts))