(****************************************************************************)
(*                                                                          *)
(*                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_confluence.
Require csubst1_defs.
Require pr3_gen_context.
Require pc3_defs.
Require pc3_props.

   Section pc3_gen_context. (************************************************)

      Lemma pc3_gen_cabbr: (c:?; t1,t2:?) (pc3 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)) ->
                           (x2:?) (subst1 d u t2 (lift (1) d x2)) ->
                           (pc3 a x1 x2).
      Proof.
      Intros; Pc3Unfold; Repeat Pr3GenContext.
      Subst1Confluence; Rewrite H3 in H5; Clear H3 x3; XDEAuto 2.
      Qed.

   End pc3_gen_context.