DEFINITION lift1_sort()
TYPE =
       ∀n:nat.∀is:PList.(eq T (lift1 is (TSort n)) (TSort n))
BODY =
        assume n: nat
        assume is: PList
          we proceed by induction on is to prove eq T (lift1 is (TSort n)) (TSort n)
             case PNil : ⇒
                the thesis becomes eq T (lift1 PNil (TSort n)) (TSort n)
                   by (refl_equal . .)
                   we proved eq T (TSort n) (TSort n)
eq T (lift1 PNil (TSort n)) (TSort n)
             case PCons : n0:nat n1:nat p:PList ⇒
                the thesis becomes eq T (lift1 (PCons n0 n1 p) (TSort n)) (TSort n)
                (H) by induction hypothesis we know eq T (lift1 p (TSort n)) (TSort n)
                   by (refl_equal . .)
                   we proved eq T (TSort n) (TSort n)
                   that is equivalent to eq T (lift n0 n1 (TSort n)) (TSort n)
                   by (eq_ind_r . . . previous . H)
                   we proved eq T (lift n0 n1 (lift1 p (TSort n))) (TSort n)
eq T (lift1 (PCons n0 n1 p) (TSort n)) (TSort n)
          we proved eq T (lift1 is (TSort n)) (TSort n)
       we proved ∀n:nat.∀is:PList.(eq T (lift1 is (TSort n)) (TSort n))