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).
+ | 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).
+ Theorem pr1_pr0: (t1,t2:?) (pr0 t1 t2) -> (pr1 t1 t2).
XEAuto.
Qed.
- Theorem pr1_t : (t2,t1:?) (pr1 t1 t2) ->
+ Theorem pr1_t: (t2,t1:?) (pr1 t1 t2) ->
(t3:?) (pr1 t2 t3) -> (pr1 t1 t3).
- Intros t2 t1 H; XElim H; XEAuto.
+ 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 : ltlc.
+ Hints Resolve pr1_pr0 pr1_t pr1_tail_1 pr1_tail_2 : ltlc.