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

Require getl_props.
Require csubv_defs.
Require aprem_defs.
Require arity_defs.
Require arity_props.
Require csuba_defs.

   Section csuba_props. (*****************************************************)

      Hints Resolve asucc_inj arity_repl : ld.

      Lemma csuba_arity: (g:?; c1:?; t:?; a:?) (arity g c1 t a) ->
                         (c2:?) (csuba g c1 c2) -> (arity g c2 t a).
      Proof.
      Intros until 1; XElim H; Clear c1 t a; Intros.
(* case 1: arity_sort *)
      XAuto.
(* case 2: arity_abbr *)
      CSubAGetL; XDEAuto 3.
(* case 3: arity_abst *)
      CSubAGetL; [ XDEAuto 3 | Idtac ].
      ArityDis; Subst; XDEAuto 4.
(* case 4: arity_bind *)
      XDEAuto 5.
(* case 5: arity_head *)
      XAuto.
(* case 6: arity_appl *)
      XDEAuto 4.
(* case 7: arity_cast *)
      XDEAuto 4.
(* case 8: arity_repl *)
      XDEAuto 3.
      Qed.

      Lemma csuba_arity_rev: (g:?; c1:?; t:?; a:?) (arity g c1 t a) ->
                             (c2:?) (csuba g c2 c1) -> (csubv c2 c1) ->
                                   (arity g c2 t a).
      Proof.
      Intros until 1; XElim H; Clear c1 t a; Intros.
(* case 1: arity_sort *)
      XAuto.
(* case 2: arity_abbr *)
      CSubAGetL.
(* case 2.1: Abbr *)
      CSubVGetL; GetLDis; XInv; Subst; XDEAuto 3.
(* case 2.2: Abst *)
      ArityDis; Subst; XDEAuto 4.
(* case 2.3: Void *)
      CSubVGetL; GetLDis; XInv.
(* case 3: arity_abst *)
      CSubAGetL; CSubVGetL; GetLDis; XInv; Subst; XDEAuto 3.
(* case 4: arity_bind *)
      XDEAuto 6.
(* case 5: arity_head *)
      XAuto.
(* case 6: arity_appl *)
      XDEAuto 4.
(* case 7: arity_cast *)
      XDEAuto 4.
(* case 8: arity_repl *)
      XDEAuto 3.
      Qed.

   End csuba_props.

   Section arity_props. (****************************************************)

      Hints Resolve csuba_arity_rev : ld.

      Theorem arity_appls_appl: (g:?; c:?; v:?; a1:?) (arity g c v a1) ->
                                (u:?) (arity g c u (asucc g a1)) ->
                                (t:?; vs:?; a2:?) (arity g c (THeads (Flat Appl) vs (THead (Bind Abbr) v t)) a2) ->
                                (arity g c (THeads (Flat Appl) vs (THead (Flat Appl) v (THead (Bind Abst) u t))) a2).
      Proof.
      XElim vs; Simpl; Intros.
(* case 1: nil *)
      ArityGenBase; ArityDis; XDEAuto 6.
(* case 2: cons *)
      ArityGenBase; XDEAuto 3.
      Qed.

   End arity_props.