ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v
index 1e5b04249a12ebfe63871e11455fcffc8e5e0202..df6764b3f6022919b579f8809209081ed765508a 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v
@@ -134,6 +134,12 @@ Require Export pr2_defs.
       Intros until 1; XElim H; XEAuto.
       Qed.
 
+      Theorem pr3_thin_dx: (c:?; t1,t2:?) (pr3 c t1 t2) ->
+                           (u:?; f:?) (pr3 c (TTail (Flat f) u t1)
+                                             (TTail (Flat f) u t2)).
+      Intros; XElim H; XEAuto.
+      Qed.
+
       Theorem pr3_tail_1: (c:?; u1,u2:?) (pr3 c u1 u2) ->
                           (k:?; t:?) (pr3 c (TTail k u1 t) (TTail k u2 t)).
       Intros until 1; XElim H; Intros.
@@ -185,4 +191,4 @@ Require Export pr2_defs.
    End pr3_props.
 
       Hints Resolve pr3_pr2 pr3_t pr3_pr1
-                    pr3_tail_12 pr3_tail_21 pr3_shift : ltlc.
+                    pr3_thin_dx pr3_tail_12 pr3_tail_21 pr3_shift : ltlc.