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

Require drop1_props.
Require getl_props.
Require aprem_defs.
Require arity_props.
Require nf2_props.
Require sc3_props.
Require csubc_defs.
Require csubc_props.

   Section sc3_arity. (******************************************************)

      Hints Resolve drop1_trans sc3_repl sc3_abbr csubc_arity_conf : ld.

      Lemma sc3_arity_csubc: (g:?; c1:?; t:?; a:?) (arity g c1 t a) ->
                             (d1:?; is:?) (drop1 is d1 c1) ->
                             (c2:?) (csubc g d1 c2) ->
                             (sc3 g a c2 (lift1 is t)).
      Proof.
      Intros until 1; XElim H; Clear c1 t a; Intros.
(* case 1: arity_sort *)
      Simpl; Rewrite lift1_sort; XDEAuto 3.
(* case 2: arity_abbr *)
      GetLDrop; GetLXDis; CSubCGetL; CSubCGenBase; XInv.
      XPoseClear H0 '(sc3_abbr g a TNil); Simpl in H0.
      Rewrite lift1_lref; EApply H0; [ Idtac | XDEAuto 2 ].
      Rewrite <- lift1_free; Try Rewrite <- lift1_cons_tail; XDEAuto 3.
(* case 3: arity_abst *)
      Move H after H3; NonLinear; GetLDrop; GetLXDis; CSubCGetL; CSubCGenBase.
(* case 3.1: csubc_head *)
      XPoseClear H1 '(sc3_abst g a TNil); Simpl in H1.
      Rewrite lift1_lref; Apply H1; Clear H1;
      [ EApply csubc_arity_conf; Try Rewrite <- lift1_lref; XDEAuto 3
      | XDEAuto 2 | XAuto
      ].
(* case 3.2: csubc_abst *)
      Clear H9; GetLDrop.
      XPoseClear H1 '(sc3_abbr g a TNil); Simpl in H1.
      Rewrite lift1_lref; EApply H1; [ Idtac | XDEAuto 2 ].
      Clear H H1 H2 H3 H4 H5 H11.
      XPoseClear H0 '(arity_lift1 ? ? ? ? ? ? H6 H0); Clear H6.
      XPoseClear H12 '(sc3_arity_gen ? ? ? ? H12).
      ArityDis; ASuccDis; Clear H0; XDEAuto 3.
(* case 3.3: csubc_void *)
      XInv.
(* case 4: arity_bind *)
      XPoseClear H '(sc3_bind g ? H a1 a2 TNil); Simpl in H.
      Rewrite lift1_bind; XDEAuto 6.
(* case 5: arity_head *)
      Simpl; Intros; Rewrite lift1_bind.
      Split; [ XDEAuto 6 | Clear H H1; Intros; Rewrite lift1_bind ].
      XPose H5 '(sc3_appl g a1 a2 TNil); Simpl in H5.
      Apply H5; [ Clear H5 | XAuto | XDEAuto 3 ].
      LApply (sc3_bind g Abbr); [ Intros H5 | XAuto ].
      XPoseClear H5 '(H5 a1 a2 TNil); Simpl in H5.
      Apply H5; Clear H5; [ CSubCDrop1 | XAuto ].
      Rewrite lift1_lift1; Rewrite papp_ss.
      EApply H2; [ Idtac | EApply csubc_abst; XDEAuto 3 ].
      Clear H H0 H2 H6 a1 a2 c2 d g t w; XDEAuto 3.
(* case 6: arity_appl *)
      XPoseClear H0 '(H0 ? ? H3 ? H4).
      XPoseClear H2 '(H2 ? ? H3 ? H4); Clear H3 H4.
      Simpl in H2; XDecompose H2.
      XPoseClear H4 '(H4 ? ? H0 PNil); Simpl in H4; Clear H0.
      Rewrite lift1_flat; XAuto.
(* case 7: arity_cast *)
      XPoseClear H '(sc3_cast g a TNil); Simpl in H.
      Rewrite lift1_flat; XDEAuto 4.
(* case 8: arity_repl *)
      XDEAuto 3.
      Qed.

      Lemma sc3_arity: (g:?; c:?; t:?; a:?)
                       (arity g c t a) -> (sc3 g a c t).
      Proof.
      Intros.
      XPoseClear H '(sc3_arity_csubc ? ? ? ? H c PNil).
      XAuto.
      Qed.

   End sc3_arity.

      Hints Resolve sc3_arity : ld.