X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr3_defs.v;h=df6764b3f6022919b579f8809209081ed765508a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=1e5b04249a12ebfe63871e11455fcffc8e5e0202;hpb=a8052b7482d5573eca2776ea11cb7a4b06236fbd;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v
index 1e5b04249..df6764b3f 100644
--- 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.