DEFINITION lifts1_xhg()
TYPE =
       ∀hds:PList
         .∀ts:TList
           .eq
             TList
             lifts1 (Ss hds) (lifts (S O) O ts)
             lifts (S O) O (lifts1 hds ts)
BODY =
        assume hds: PList
        assume ts: TList
          we proceed by induction on ts to prove 
             eq
               TList
               lifts1 (Ss hds) (lifts (S O) O ts)
               lifts (S O) O (lifts1 hds ts)
             case TNil : ⇒
                the thesis becomes 
                eq
                  TList
                  lifts1 (Ss hds) (lifts (S O) O TNil)
                  lifts (S O) O (lifts1 hds TNil)
                   by (refl_equal . .)
                   we proved eq TList TNil TNil

                      eq
                        TList
                        lifts1 (Ss hds) (lifts (S O) O TNil)
                        lifts (S O) O (lifts1 hds TNil)
             case TCons : t:T t0:TList ⇒
                the thesis becomes 
                eq
                  TList
                  lifts1 (Ss hds) (lifts (S O) O (TCons t t0))
                  lifts (S O) O (lifts1 hds (TCons t t0))
                (H) by induction hypothesis we know 
                   eq TList (lifts1 (Ss hds) (lifts (S O) O t0)) (lifts (S O) O (lifts1 hds t0))
                   (h1) 
                      by (refl_equal . .)
                      we proved 
                         eq
                           TList
                           TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O (lifts1 hds t0))
                           TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O (lifts1 hds t0))
                      by (eq_ind_r . . . previous . H)

                         eq
                           TList
                           TCons (lift (S O) O (lift1 hds t)) (lifts1 (Ss hds) (lifts (S O) O t0))
                           TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O (lifts1 hds t0))
                   end of h1
                   (h2) 
                      by (lift1_xhg . .)
eq T (lift1 (Ss hds) (lift (S O) O t)) (lift (S O) O (lift1 hds t))
                   end of h2
                   by (eq_ind_r . . . h1 . h2)
                   we proved 
                      eq
                        TList
                        TCons
                          lift1 (Ss hds) (lift (S O) O t)
                          lifts1 (Ss hds) (lifts (S O) O t0)
                        TCons (lift (S O) O (lift1 hds t)) (lifts (S O) O (lifts1 hds t0))

                      eq
                        TList
                        lifts1 (Ss hds) (lifts (S O) O (TCons t t0))
                        lifts (S O) O (lifts1 hds (TCons t t0))
          we proved 
             eq
               TList
               lifts1 (Ss hds) (lifts (S O) O ts)
               lifts (S O) O (lifts1 hds ts)
       we proved 
          ∀hds:PList
            .∀ts:TList
              .eq
                TList
                lifts1 (Ss hds) (lifts (S O) O ts)
                lifts (S O) O (lifts1 hds ts)