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

Require Export pr0_defs.
Require Export pr1_defs.

      Definition pc1 := [t1,t2:?] (EX t | (pr1 t1 t) & (pr1 t2 t)).

      Hints Unfold pc1 : ld.

      Tactic Definition Pc1Unfold := (
         Match Context With
            | [ H: (pc1 ?2 ?3) |- ? ] -> Unfold pc1 in H; XDecompose H
         ).

   Section pc1_props. (******************************************************)

      Lemma pc1_pr0_r: (t1,t2:?) (pr0 t1 t2) -> (pc1 t1 t2).
      Proof.
      XDEAuto 4.
      Qed.

      Lemma pc1_pr0_x: (t1,t2:?) (pr0 t2 t1) -> (pc1 t1 t2).
      Proof.
      XDEAuto 4.
      Qed.

      Lemma pc1_refl: (t:?) (pc1 t t).
      Proof.
      XDEAuto 3.
      Qed.

      Hints Resolve pr1_sing : ld.

      Lemma pc1_pr0_u: (t2,t1:?) (pr0 t1 t2) ->
                       (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
      Proof.
      Intros; Pc1Unfold; XDEAuto 4.
      Qed.

      Lemma pc1_s: (t2,t1:?) (pc1 t1 t2) -> (pc1 t2 t1).
      Proof.
      Intros; Pc1Unfold; XDEAuto 3.
      Qed.

      Lemma pc1_head_1: (u1,u2:?) (pc1 u1 u2) ->
                        (t:?; k:?) (pc1 (THead k u1 t) (THead k u2 t)).
      Proof.
      Intros; Pc1Unfold; XDEAuto 5.
      Qed.

      Lemma pc1_head_2: (t1,t2:?) (pc1 t1 t2) ->
                        (u:?; k:?) (pc1 (THead k u t1) (THead k u t2)).
      Proof.
      Intros; Pc1Unfold; XDEAuto 5.
      Qed.

   End pc1_props.

      Hints Resolve pc1_refl pc1_pr0_r pc1_pr0_x pc1_head_1 pc1_head_2 : ld.