(****************************************************************************)
(*                                                                          *)
(*                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_defs.
Require subst1_confluence.
Require getl_props.
Require pr0_subst1.
Require pr2_defs.

   Section pr2_subst1_props. (***********************************************)

      Lemma pr2_delta1: (c,d:?; u:?; i:?) (getl i c (CHead d (Bind Abbr) u)) ->
                        (t1,t2:?) (pr0 t1 t2) -> (t:?) (subst1 i u t2 t) ->
                        (pr2 c t1 t).
      Proof.
      Intros; XElim H1; Clear t; XDEAuto 2.
      Qed.

      Hints Resolve sym_not_eq pr2_delta1 : ld.

      Lemma pr2_subst1: (c,e:?; v:?; i:?) (getl i c (CHead e (Bind Abbr) v)) ->
                        (t1,t2:?) (pr2 c t1 t2) ->
                        (w1:?) (subst1 i v t1 w1) ->
                        (EX w2 | (pr2 c w1 w2) & (subst1 i v t2 w2)).
      Proof.
      Intros until 2; InsertEq H0 c; XElim H0; Clear y t1 t2;
      Intros; Subst; Pr0Subst1.
(* case 1: pr2_free *)
      XDEAuto 3.
(* case 2: pr2_delta *)
      Apply (neq_eq_e i i0); Intros; Subst.
(* case 2.1: i <> i0 *)
      Subst1Confluence; XDEAuto 3.
(* case 2.2: i = i0 *)
      GetLDis; XInv; Subst; Subst1Confluence; XDEAuto 3.
      Qed.

   End pr2_subst1_props.

      Hints Resolve pr2_delta1 : ld.

      Tactic Definition Pr2Subst1 := (
         Match Context With
            | [ H0: (getl ?1 ?2 (CHead ?3 (Bind Abbr) ?4));
                H1: (pr2 ?2 ?5 ?6); H3: (subst1 ?1 ?4 ?5 ?7) |- ? ] ->
               LApply (pr2_subst1 ?2 ?3 ?4 ?1); [ Intros H_x | XAuto ];
               LApply (H_x ?5 ?6); [ Clear H_x H1; Intros H1 | XAuto ];
               LApply (H1 ?7); [ Clear H1; Intros H1 | XAuto ];
               XElim H1; Intros
         ).