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

Require pr1_confluence.
Require pc1_defs.

   Section pc1_trans. (******************************************************)

      Hints Resolve pr1_t : ld.

      Theorem pc1_t: (t2,t1:?) (pc1 t1 t2) ->
                     (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
      Proof.
      Intros; Repeat Pc1Unfold; Pr1Confluence; XDEAuto 5.
      Qed.

      Lemma pc1_pr0_u2: (t0,t1:?) (pr0 t0 t1) ->
                        (t2:?) (pc1 t0 t2) -> (pc1 t1 t2).
      Proof.
      Intros; Apply (pc1_t t0); XAuto.
      Qed.

      Theorem pc1_head: (u1,u2:?) (pc1 u1 u2) -> (t1,t2:?) (pc1 t1 t2) ->
                        (k:?) (pc1 (THead k u1 t1) (THead k u2 t2)).
      Proof.
      Intros; EApply pc1_t; [ EApply pc1_head_1 | EApply pc1_head_2 ]; XAuto.
      Qed.

   End pc1_trans.

      Hints Resolve pc1_head : ld.