(****************************************************************************)
(*                                                                          *)
(*                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 nf2_defs.
Require nf2_props.
Require pc3_props.
Require pc3_gen.
Require ty3_defs.
Require ty3_gen.

      Definition ex1_c := (CHead
                           (CHead
                            (CHead (CSort (0)) (Bind Abst) (TSort (0)))
                            (Bind Abst) (TSort (0))
                           ) (Bind Abst) (TLRef (0))
                          ).

      Definition ex1_t := (THead (Flat Appl) (TLRef (0))
                                 (THead (Bind Abst) (TLRef (2)) (TSort (0)))
                          ).

   Section ex1. (************************************************************)

      Remark leq_sort_SS: (g:?; k,n:?)
                          (leq g (ASort k n)
                                 (asucc g (asucc g (ASort (S (S k)) n)))
                          ).
      Proof.
      XAuto.
      Qed.

      Hints Resolve leq_sort_SS arity_repl : ld.

      Lemma ex1_arity: (g:?) (arity g ex1_c ex1_t (ASort (0) (0))).
      Proof.
      Unfold ex1_c ex1_t; Intros.
      EApply arity_appl; XDEAuto 6.
      Qed.

      Hints Resolve ex2_sym : ld.

      Lemma ex1_ty3: (g:?; u:?) (ty3 g ex1_c ex1_t u) -> (P:Prop) P.
      Proof.
      Unfold ex1_c ex1_t; Intros.
      Repeat Ty3GenBase; Repeat GetLGenBase; Repeat ClearGenBase; XInv; Subst;
      DropGenBase; Simpl in H2; DropGenBase; Subst; ClearGenBase; XInv; Subst.
      Repeat Ty3GenBase; Repeat GetLGenBase; Repeat ClearGenBase; XInv; Subst.
      Repeat Ty3GenBase; Clear H H2 H3 H4 H6 H7 u x4 x6 x7 x8 x10.
      Pc3Gen; Clear H0 H5 x1 x5.
      Pc3T; Clear H H1 x0.
      Rewrite lift_lref_ge in H0; [ Pc3Unfold | XAuto ].
      LApply (nf2_pr3_unfold ? ? ? H); [ Clear H; Intros | XDEAuto 4 ].
      LApply (nf2_pr3_unfold ? ? ? H1); [ Clear H1; Intros | XDEAuto 4 ].
      Subst; XInv.
      Qed.

   End ex1.