DEFINITION lift1_bind()
TYPE =
       ∀b:B
         .∀hds:PList
           .∀u:T
             .∀t:T
               .eq
                 T
                 lift1 hds (THead (Bind b) u t)
                 THead (Bind b) (lift1 hds u) (lift1 (Ss hds) t)
BODY =
        assume b: B
        assume hds: PList
          we proceed by induction on hds to prove 
             ∀u:T
               .∀t:T
                 .eq
                   T
                   lift1 hds (THead (Bind b) u t)
                   THead (Bind b) (lift1 hds u) (lift1 (Ss hds) t)
             case PNil : ⇒
                the thesis becomes 
                ∀u:T
                  .∀t:T
                    .eq
                      T
                      lift1 PNil (THead (Bind b) u t)
                      THead (Bind b) (lift1 PNil u) (lift1 (Ss PNil) t)
                    assume u: T
                    assume t: T
                      by (refl_equal . .)
                      we proved eq T (THead (Bind b) u t) (THead (Bind b) u t)
                      that is equivalent to 
                         eq
                           T
                           lift1 PNil (THead (Bind b) u t)
                           THead (Bind b) (lift1 PNil u) (lift1 (Ss PNil) t)

                      ∀u:T
                        .∀t:T
                          .eq
                            T
                            lift1 PNil (THead (Bind b) u t)
                            THead (Bind b) (lift1 PNil u) (lift1 (Ss PNil) t)
             case PCons : n:nat n0:nat p:PList ⇒
                the thesis becomes 
                ∀u:T
                  .∀t:T
                    .eq
                      T
                      lift n n0 (lift1 p (THead (Bind b) u t))
                      THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))
                (H) by induction hypothesis we know 
                   ∀u:T
                     .∀t:T
                       .eq
                         T
                         lift1 p (THead (Bind b) u t)
                         THead (Bind b) (lift1 p u) (lift1 (Ss p) t)
                    assume u: T
                    assume t: T
                      (h1) 
                         (h1) 
                            by (refl_equal . .)

                               eq
                                 T
                                 THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))
                                 THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))
                         end of h1
                         (h2) 
                            by (lift_bind . . . . .)

                               eq
                                 T
                                 lift n n0 (THead (Bind b) (lift1 p u) (lift1 (Ss p) t))
                                 THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))
                         end of h2
                         by (eq_ind_r . . . h1 . h2)

                            eq
                              T
                              lift n n0 (THead (Bind b) (lift1 p u) (lift1 (Ss p) t))
                              THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))
                      end of h1
                      (h2) 
                         by (H . .)

                            eq
                              T
                              lift1 p (THead (Bind b) u t)
                              THead (Bind b) (lift1 p u) (lift1 (Ss p) t)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved 
                         eq
                           T
                           lift n n0 (lift1 p (THead (Bind b) u t))
                           THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))
                      that is equivalent to 
                         eq
                           T
                           lift1 (PCons n n0 p) (THead (Bind b) u t)
                           THead (Bind b) (lift1 (PCons n n0 p) u) (lift1 (Ss (PCons n n0 p)) t)

                      ∀u:T
                        .∀t:T
                          .eq
                            T
                            lift n n0 (lift1 p (THead (Bind b) u t))
                            THead (Bind b) (lift n n0 (lift1 p u)) (lift n (S n0) (lift1 (Ss p) t))
          we proved 
             ∀u:T
               .∀t:T
                 .eq
                   T
                   lift1 hds (THead (Bind b) u t)
                   THead (Bind b) (lift1 hds u) (lift1 (Ss hds) t)
       we proved 
          ∀b:B
            .∀hds:PList
              .∀u:T
                .∀t:T
                  .eq
                    T
                    lift1 hds (THead (Bind b) u t)
                    THead (Bind b) (lift1 hds u) (lift1 (Ss hds) t)