DEFINITION lift1_lref()
TYPE =
       ∀hds:PList.∀i:nat.(eq T (lift1 hds (TLRef i)) (TLRef (trans hds i)))
BODY =
       assume hds: PList
          we proceed by induction on hds to prove ∀i:nat.(eq T (lift1 hds (TLRef i)) (TLRef (trans hds i)))
             case PNil : ⇒
                the thesis becomes ∀i:nat.(eq T (lift1 PNil (TLRef i)) (TLRef (trans PNil i)))
                   assume i: nat
                      by (refl_equal . .)
                      we proved eq T (TLRef i) (TLRef i)
                      that is equivalent to eq T (lift1 PNil (TLRef i)) (TLRef (trans PNil i))
∀i:nat.(eq T (lift1 PNil (TLRef i)) (TLRef (trans PNil i)))
             case PCons : n:nat n0:nat p:PList ⇒
                the thesis becomes 
                ∀i:nat
                  .eq
                    T
                    lift n n0 (lift1 p (TLRef i))
                    TLRef
                      <λb:bool.nat>
                        CASE blt (trans p i) n0 OF
                          true⇒trans p i
                        | false⇒plus (trans p i) n
                (H) by induction hypothesis we know ∀i:nat.(eq T (lift1 p (TLRef i)) (TLRef (trans p i)))
                   assume i: nat
                      (h1) 
                         by (refl_equal . .)
                         we proved 
                            eq
                              T
                              TLRef
                                <λb:bool.nat>
                                  CASE blt (trans p i) n0 OF
                                    true⇒trans p i
                                  | false⇒plus (trans p i) n
                              TLRef
                                <λb:bool.nat>
                                  CASE blt (trans p i) n0 OF
                                    true⇒trans p i
                                  | false⇒plus (trans p i) n

                            eq
                              T
                              lift n n0 (TLRef (trans p i))
                              TLRef
                                <λb:bool.nat>
                                  CASE blt (trans p i) n0 OF
                                    true⇒trans p i
                                  | false⇒plus (trans p i) n
                      end of h1
                      (h2) 
                         by (H .)
eq T (lift1 p (TLRef i)) (TLRef (trans p i))
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved 
                         eq
                           T
                           lift n n0 (lift1 p (TLRef i))
                           TLRef
                             <λb:bool.nat>
                               CASE blt (trans p i) n0 OF
                                 true⇒trans p i
                               | false⇒plus (trans p i) n
                      that is equivalent to 
                         eq T (lift1 (PCons n n0 p) (TLRef i)) (TLRef (trans (PCons n n0 p) i))

                      ∀i:nat
                        .eq
                          T
                          lift n n0 (lift1 p (TLRef i))
                          TLRef
                            <λb:bool.nat>
                              CASE blt (trans p i) n0 OF
                                true⇒trans p i
                              | false⇒plus (trans p i) n
          we proved ∀i:nat.(eq T (lift1 hds (TLRef i)) (TLRef (trans hds i)))
       we proved ∀hds:PList.∀i:nat.(eq T (lift1 hds (TLRef i)) (TLRef (trans hds i)))