(****************************************************************************)
(*                                                                          *)
(*                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 fsubst0_defs.
Require arity_defs.
Require arity_props.

   Section arity_subst0. (***************************************************)

      Hints Resolve le_S_n getl_drop arity_repl : ld.

      Lemma arity_fsubst0: (g:?; c1:?; t1:?; a:?) (arity g c1 t1 a) ->
                           (d1:?; u:?; i:?) (getl i c1 (CHead d1 (Bind Abbr) u)) ->
                           (c2:?; t2:?) (fsubst0 i u c1 t1 c2 t2) ->
                           (arity g c2 t2 a).
      Proof.
      Intros until 1; XElim H; Clear c1 t1 a; Intros;
      FSubst0GenBase; Subst.
(* case 1.1: arity_sort, fsubst0_snd *)
      Subst0GenBase.
(* case 1.2: arity_sort, fsubst0_fst *)
      XDEAuto 2.
(* case 1.3: arity_sort, fsubst0_both *)
      Subst0GenBase.
(* case 2.1: arity_abbr, fsubst0_snd *)
      Subst0GenBase; Subst; GetLDis; XInv; Subst; XDEAuto 3.
(* case 2.2: arity_abbr, fsubst0_snd *)
      Apply (lt_le_e i i0); Intros.
(* case 2.2.1: i < i0 *)
      GetLDis; CSubst0GetL;
      Try (
         Rewrite (minus_x_Sy i0 i) in H4; [ Idtac | XAuto ];
         GetLGenBase; XInv; Subst
      ); XDEAuto 4.
(* case 2.2.2: i >= i0 *)
      CSubst0GetL; XDEAuto 2.
(* case 2.3: arity_abbr, fsubst0_both *)
      Subst0GenBase; Subst; GetLDis; XInv; Subst; CSubst0GetL; XDEAuto 3.
(* case 3.1: arity_abst, fsubst0_snd *)
      Subst0GenBase; Subst; GetLDis; XInv; Subst; XDEAuto 3.
(* case 3.2: arity_abst, fsubst0_snd *)
      Apply (lt_le_e i i0); Intros.
(* case 3.2.1: i < i0 *)
      GetLDis; CSubst0GetL;
      Try (
         Rewrite (minus_x_Sy i0 i) in H4; [ Idtac | XAuto ];
         GetLGenBase; XInv; Subst
      ); XDEAuto 4.
(* case 3.2.2: i >= i0 *)
      CSubst0GetL; XDEAuto 2.
(* case 3.3: arity_abst, fsubst0_both *)
      Subst0GenBase; Subst; GetLDis; XInv; Subst; CSubst0GetL; XDEAuto 3.
(* case 4.1: arity_bind, fsubst0_snd *)
      Subst0GenBase; Subst; EApply arity_bind; XDEAuto 5.
(* case 4.2: arity_bind, fsubst0_fst *)
      EApply arity_bind; XDEAuto 5.
(* case 4.3: arity_bind, fsubst0_both *)
      Subst0GenBase; Subst; EApply arity_bind; XDEAuto 5.
(* case 5.1: arity_head, fsubst0_snd *)
      Subst0GenBase; Subst; EApply arity_head; XDEAuto 5.
(* case 5.2: arity_head, fsubst0_fst *)
      EApply arity_head; XDEAuto 5.
(* case 5.3: arity_head, fsubst0_both *)
      Subst0GenBase; Subst; EApply arity_head; XDEAuto 5.
(* case 6.1: arity_appl, fsubst0_snd *)
      Subst0GenBase; Subst; EApply arity_appl; XDEAuto 3.
(* case 6.2: arity_appl, fsubst0_fst *)
      EApply arity_appl; XDEAuto 3.
(* case 6.3: arity_appl, fsubst0_both *)
      Subst0GenBase; Subst; EApply arity_appl; XDEAuto 3.
(* case 7.1: arity_cast, fsubst0_snd *)
      Subst0GenBase; Subst; EApply arity_cast; XDEAuto 3.
(* case 7.2: arity_cast, fsubst0_fst *)
      EApply arity_cast; XDEAuto 3.
(* case 7.3: arity_cast, fsubst0_both *)
      Subst0GenBase; Subst; EApply arity_cast; XDEAuto 3.
(* case 8.1: arity_repl, fsubst0_snd *)
      XDEAuto 4.
(* case 8.2: arity_repl, fsubst0_fst *)
      XDEAuto 4.
(* case 8.3: arity_repl, fsubst0_both *)
      XDEAuto 4.
      Qed.

      Hints Resolve arity_fsubst0 : ld.

      Lemma arity_subst0: (g:?; c:?; t1:?; a:?) (arity g c t1 a) ->
                          (d:?; u:?; i:?) (getl i c (CHead d (Bind Abbr) u)) ->
                          (t2:?) (subst0 i u t1 t2) ->
                          (arity g c t2 a).
      Proof.
      XDEAuto 3.
      Qed.

   End arity_subst0.