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

Require subst1_lift.
Require csubst1_defs.

   Section csubst1_props. (**************************************************)

      Lemma getl_csubst1: (d:?; c,e:?; u:?) (getl d c (CHead e (Bind Abbr) u)) ->
                          (EX a0 a | (csubst1 d u c a0) & (drop (1) d a0 a)).
      Proof.
      XElim d; XElim c; Try NewInduction k; Intros; GetLGenBase.
(* case 1: d = 0, CHead Bind *)
      ClearGenBase; XInv; Subst; XDEAuto 3.
(* case 2: d = 0, CHead Flat *)
      ClearGenBase; XDecomPose '(subst1_ex u t (0)).
      LApply (H e u); [ Clear H H0; Intros H | XDEAuto 2 ].
      XDecompose H; XDEAuto 4.
(* case 3: d > 0, CHead Bind *)
      XDecomPose '(subst1_ex u t n).
      LApply (H c e u); [ Clear H H0 H1; Intros H | XAuto ].
      XDecompose H; XDEAuto 4.
(* case 4: d > 0, CHead Flat *)
      XDecomPose '(subst1_ex u t (S n)).
      LApply (H0 e u); [ Clear H H0 H1; Intros H0 | XAuto ].
      XDecompose H0; XDEAuto 4.
      Qed.

   End csubst1_props.

      Tactic Definition GetLCSubst1 := (
         Match Context With
            | [ H: (getl ?4 ?1 (CHead ?2 (Bind Abbr) ?3)) |- ? ] ->
               LApply (getl_csubst1 ?4 ?1 ?2 ?3); [ Intros H_x | XAuto ];
               XDecompose H_x
         ).