ocaml 3.09 transition

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / pr1_defs.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr1_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr1_defs.v
index 986b5948937cf5c5768e74447d8de7020194a75a..ed05b0e5d88202b938eb5021dcc710e619ea58d6 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pr1_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr1_defs.v
@@ -3,22 +3,32 @@
 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.