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

Require csubst1_defs.
Require pr2_gen_context.
Require pr3_defs.

   Section pr3_gen_context. (************************************************)

      Hints Resolve pr3_sing : ld.

      Lemma pr3_gen_cabbr: (c:?; t1,t2:?) (pr3 c t1 t2) -> (e:?; u:?; d:?)
                           (getl d c (CHead e (Bind Abbr) u)) ->
                           (a0:?) (csubst1 d u c a0) ->
                           (a:?) (drop (1) d a0 a) ->
                           (x1:?) (subst1 d u t1 (lift (1) d x1)) ->
                           (EX x2 | (subst1 d u t2 (lift (1) d x2)) &
                                    (pr3 a x1 x2)
                           ).
      Proof.
      Intros until 1; XElim H; Intros.
(* case 1: pr3_refl *)
      XDEAuto 2.
(* case 1: pr3_refl *)
      Pr2GenContext.
      LApply (H1 e u d); [ Clear H1; Intros H1 | XAuto ].
      LApply (H1 a0); [ Clear H1; Intros H1 | XAuto ].
      LApply (H1 a); [ Clear H1; Intros H1 | XAuto ].
      LApply (H1 x); [ Clear H1; Intros H1 | XAuto ].
      XElim H1; XDEAuto 3.
      Qed.

   End pr3_gen_context.

      Tactic Definition Pr3GenContext := (
         Match Context With
            | [ H0: (pr3 ?1 ?2 ?3); H1: (getl ?4 ?1 (CHead ?5 (Bind Abbr) ?6));
                H2: (csubst1 ?4 ?6 ?1 ?7); H3: (drop (1) ?4 ?7 ?8);
                H4: (subst1 ?4 ?6 ?2 (lift (1) ?4 ?9)) |- ? ] ->
               LApply (pr3_gen_cabbr ?1 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
               LApply (H0 ?5 ?6 ?4); [ Clear H0; Intros H0 | XAuto ];
               LApply (H0 ?7); [ Clear H0; Intros H0 | XAuto ];
               LApply (H0 ?8); [ Clear H0; Intros H0 | XAuto ];
               LApply (H0 ?9); [ Clear H0 H4; Intros H0 | XAuto ];
               XElim H0; Intros
            | [ |- ? ] -> Pr2GenContext
         ).