DEFINITION papp_ss()
TYPE =
       ∀is1:PList.∀is2:PList.(eq PList (papp (Ss is1) (Ss is2)) (Ss (papp is1 is2)))
BODY =
       assume is1: PList
          we proceed by induction on is1 to prove ∀is2:PList.(eq PList (papp (Ss is1) (Ss is2)) (Ss (papp is1 is2)))
             case PNil : ⇒
                the thesis becomes ∀is2:PList.(eq PList (papp (Ss PNil) (Ss is2)) (Ss (papp PNil is2)))
                   assume is2: PList
                      by (refl_equal . .)
                      we proved eq PList (Ss is2) (Ss is2)
                      that is equivalent to eq PList (papp (Ss PNil) (Ss is2)) (Ss (papp PNil is2))
∀is2:PList.(eq PList (papp (Ss PNil) (Ss is2)) (Ss (papp PNil is2)))
             case PCons : n:nat n0:nat p:PList ⇒
                the thesis becomes 
                ∀is2:PList
                  .eq
                    PList
                    PCons n (S n0) (papp (Ss p) (Ss is2))
                    PCons n (S n0) (Ss (papp p is2))
                (H) by induction hypothesis we know ∀is2:PList.(eq PList (papp (Ss p) (Ss is2)) (Ss (papp p is2)))
                   assume is2: PList
                      (h1) 
                         by (refl_equal . .)

                            eq
                              PList
                              PCons n (S n0) (Ss (papp p is2))
                              PCons n (S n0) (Ss (papp p is2))
                      end of h1
                      (h2) 
                         by (H .)
eq PList (papp (Ss p) (Ss is2)) (Ss (papp p is2))
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved 
                         eq
                           PList
                           PCons n (S n0) (papp (Ss p) (Ss is2))
                           PCons n (S n0) (Ss (papp p is2))
                      that is equivalent to 
                         eq
                           PList
                           papp (Ss (PCons n n0 p)) (Ss is2)
                           Ss (papp (PCons n n0 p) is2)

                      ∀is2:PList
                        .eq
                          PList
                          PCons n (S n0) (papp (Ss p) (Ss is2))
                          PCons n (S n0) (Ss (papp p is2))
          we proved ∀is2:PList.(eq PList (papp (Ss is1) (Ss is2)) (Ss (papp is1 is2)))
       we proved ∀is1:PList.∀is2:PList.(eq PList (papp (Ss is1) (Ss is2)) (Ss (papp is1 is2)))