(*#* #stop file *)

Require Export pr0_defs.

      Inductive pr1 : T -> T -> Prop :=
         | pr1_r: (t:?) (pr1 t t)
         | pr1_u: (t2,t1:?) (pr0 t1 t2) -> (t3:?) (pr1 t2 t3) -> (pr1 t1 t3).

      Hint pr1 : ltlc := Constructors pr1.

   Section pr1_props. (******************************************************)

      Theorem pr1_pr0: (t1,t2:?) (pr0 t1 t2) -> (pr1 t1 t2).
      XEAuto.
      Qed.

      Theorem pr1_t: (t2,t1:?) (pr1 t1 t2) ->
                      (t3:?) (pr1 t2 t3) -> (pr1 t1 t3).
      Intros until 1; XElim H; XEAuto.
      Qed.

      Theorem pr1_tail_1: (u1,u2:?) (pr1 u1 u2) -> 
                          (t:?; k:?) (pr1 (TTail k u1 t) (TTail k u2 t)).
      Intros; XElim H; XEAuto.
      Qed.

      Theorem pr1_tail_2: (t1,t2:?) (pr1 t1 t2) ->
                          (u:?; k:?) (pr1 (TTail k u t1) (TTail k u t2)).
      Intros; XElim H; XEAuto.
      Qed.

   End pr1_props.

      Hints Resolve pr1_pr0 pr1_t pr1_tail_1 pr1_tail_2 : ltlc.