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

Require arity_defs.
Require pr2_gen.
Require nf2_defs.

      Definition ex2_c := (CSort O).

      Definition ex2_t := (THead (Flat Appl) (TSort O) (TSort O)).

   Section ex2. (************************************************************)

      Lemma ex2_nf2: (nf2 ex2_c ex2_t).
      Proof.
      Unfold ex2_c ex2_t nf2; Intros.
      Repeat Pr2Gen; Subst; XInv; XAuto.
      Qed.

      Lemma ex2_arity: (g:?; a:?) (arity g ex2_c ex2_t a) -> (P:Prop) P.
      Proof.
      Unfold ex2_c ex2_t; Intros.
      Repeat ArityGenBase; LEqGenBase.
      Qed.

   End ex2.