(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require Export bg_hints.

(* NOTE: monomorphic lists of pairs of natural numbers without implicit arguments *)
      Inductive PList: Set :=
         | PNil : PList
         | PCons: nat -> nat -> PList -> PList.

      Fixpoint PConsTail [hds:PList] : nat -> nat -> PList :=
         [h0,d0:?] Cases hds of
            | PNil            => (PCons h0 d0 PNil)
            | (PCons h d hds) => (PCons h d (PConsTail hds h0 d0))
         end.

      Fixpoint Ss [hds:PList] : PList :=
         Cases hds of
            | PNil            => PNil
            | (PCons h d hds) => (PCons h (S d) (Ss hds))
         end.

      Fixpoint papp [a:PList]: PList -> PList :=
         [b:?] Cases a of
            | PNil          => b
            | (PCons h d a) => (PCons h d (papp a b))
         end.

   Section papp_props_base. (************************************************)

      Lemma papp_ss: (is1,is2:?)
                     (papp (Ss is1) (Ss is2)) = (Ss (papp is1 is2)).
      Proof.
      XElim is1; Intros; Simpl; Try Rewrite H; XAuto.
      Qed.

   End papp_props_base.