DEFINITION lift1_xhg()
TYPE =
       ∀hds:PList
         .∀t:T.(eq T (lift1 (Ss hds) (lift (S O) O t)) (lift (S O) O (lift1 hds t)))
BODY =
       assume hds: PList
          we proceed by induction on hds to prove ∀t:T.(eq T (lift1 (Ss hds) (lift (S O) O t)) (lift (S O) O (lift1 hds t)))
             case PNil : ⇒
                the thesis becomes 
                ∀t:T.(eq T (lift1 (Ss PNil) (lift (S O) O t)) (lift (S O) O (lift1 PNil t)))
                   assume t: T
                      by (refl_equal . .)
                      we proved eq T (lift (S O) O t) (lift (S O) O t)
                      that is equivalent to eq T (lift1 (Ss PNil) (lift (S O) O t)) (lift (S O) O (lift1 PNil t))

                      ∀t:T.(eq T (lift1 (Ss PNil) (lift (S O) O t)) (lift (S O) O (lift1 PNil t)))
             case PCons : h:nat d:nat p:PList ⇒
                the thesis becomes 
                ∀t:T
                  .eq
                    T
                    lift h (S d) (lift1 (Ss p) (lift (S O) O t))
                    lift (S O) O (lift h d (lift1 p t))
                (H) by induction hypothesis we know ∀t:T.(eq T (lift1 (Ss p) (lift (S O) O t)) (lift (S O) O (lift1 p t)))
                   assume t: T
                      (h1) 
                         by (refl_equal . .)
                         we proved eq nat (S d) (S d)
                         that is equivalent to eq nat (plus (S O) d) (S d)
                         we proceed by induction on the previous result to prove 
                            eq
                              T
                              lift h (S d) (lift (S O) O (lift1 p t))
                              lift (S O) O (lift h d (lift1 p t))
                            case refl_equal : ⇒
                               the thesis becomes 
                               eq
                                 T
                                 lift h (plus (S O) d) (lift (S O) O (lift1 p t))
                                 lift (S O) O (lift h d (lift1 p t))
                                  (h1) 
                                     by (refl_equal . .)

                                        eq
                                          T
                                          lift (S O) O (lift h d (lift1 p t))
                                          lift (S O) O (lift h d (lift1 p t))
                                  end of h1
                                  (h2) 
                                     by (le_O_n .)
                                     we proved le O d
                                     by (lift_d . . . . . previous)

                                        eq
                                          T
                                          lift h (plus (S O) d) (lift (S O) O (lift1 p t))
                                          lift (S O) O (lift h d (lift1 p t))
                                  end of h2
                                  by (eq_ind_r . . . h1 . h2)

                                     eq
                                       T
                                       lift h (plus (S O) d) (lift (S O) O (lift1 p t))
                                       lift (S O) O (lift h d (lift1 p t))

                            eq
                              T
                              lift h (S d) (lift (S O) O (lift1 p t))
                              lift (S O) O (lift h d (lift1 p t))
                      end of h1
                      (h2) 
                         by (H .)
eq T (lift1 (Ss p) (lift (S O) O t)) (lift (S O) O (lift1 p t))
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved 
                         eq
                           T
                           lift h (S d) (lift1 (Ss p) (lift (S O) O t))
                           lift (S O) O (lift h d (lift1 p t))
                      that is equivalent to 
                         eq
                           T
                           lift1 (Ss (PCons h d p)) (lift (S O) O t)
                           lift (S O) O (lift1 (PCons h d p) t)

                      ∀t:T
                        .eq
                          T
                          lift h (S d) (lift1 (Ss p) (lift (S O) O t))
                          lift (S O) O (lift h d (lift1 p t))
          we proved ∀t:T.(eq T (lift1 (Ss hds) (lift (S O) O t)) (lift (S O) O (lift1 hds t)))
       we proved 
          ∀hds:PList
            .∀t:T.(eq T (lift1 (Ss hds) (lift (S O) O t)) (lift (S O) O (lift1 hds t)))