(****************************************************************************)
(*                                                                          *)
(*                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 drop1_defs.
Require Export llt_defs.
Require Export arity_defs.
Require Export sn3_defs.

      Fixpoint sc3 [g:G; a:A]: C -> T -> Prop := [c,t:?] Cases a of
         | (ASort h n)   => (arity g c t (ASort h n)) /\ (sn3 c t)
         | (AHead a1 a2) => (arity g c t (AHead a1 a2)) /\
                            (d:?; w:?) (sc3 g a1 d w) -> (*#* #rb *)
                            (is:?) (drop1 is d c) ->
                            (sc3 g a2 d (THead (Flat Appl) w (lift1 is t)))
      end.

   Section sc3_props_base. (*************************************************)

      Lemma sc3_arity_gen: (g:?; c:?; t:?; a:?)
                           (sc3 g a c t) -> (arity g c t a).
      Proof.
      XElim a; Simpl; Intros.
(* case 1: ASort *)
      XDecompose H; XAuto.
(* case 2: AHead *)
      XDecompose H1; XAuto.
      Qed.

      Hints Resolve leq_sym llt_repl llt_trans arity_repl : ld.

      Lemma sc3_repl: (g:?; a1:?; c:?; t:?) (sc3 g a1 c t) ->
                      (a2:?) (leq g a1 a2) -> (sc3 g a2 c t).
      Proof.
      XElimUsing llt_wf_ind a1; XElim a2; Simpl; Intros.
(* case 1: ASort *)
      XDecompose H0; XPoseClear H2 '(arity_repl ? ? ? ? H2 ? H1).
      LEqGenBase; Simpl; XDEAuto 2.
(* case 2: AHead *)
      XDecompose H2; LEqGenBase.
      Split; [ XDEAuto 3 | Clear H H4; Intros ].
      EApply H0; [ XDEAuto 3 | Clear H0 H6 x1 | XAuto ].
      EApply H5; XDEAuto 4.
      Qed.

   End sc3_props_base.