DEFINITION lifts1_nil()
TYPE =
       ∀ts:TList.(eq TList (lifts1 PNil ts) ts)
BODY =
       assume ts: TList
          we proceed by induction on ts to prove eq TList (lifts1 PNil ts) ts
             case TNil : ⇒
                the thesis becomes eq TList (lifts1 PNil TNil) TNil
                   by (refl_equal . .)
                   we proved eq TList TNil TNil
eq TList (lifts1 PNil TNil) TNil
             case TCons : t:T t0:TList ⇒
                the thesis becomes eq TList (lifts1 PNil (TCons t t0)) (TCons t t0)
                (H) by induction hypothesis we know eq TList (lifts1 PNil t0) t0
                   by (refl_equal . .)
                   we proved eq TList (TCons t t0) (TCons t t0)
                   by (eq_ind_r . . . previous . H)
                   we proved eq TList (TCons t (lifts1 PNil t0)) (TCons t t0)
eq TList (lifts1 PNil (TCons t t0)) (TCons t t0)
          we proved eq TList (lifts1 PNil ts) ts
       we proved ∀ts:TList.(eq TList (lifts1 PNil ts) ts)