X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr1_defs.v;h=ed05b0e5d88202b938eb5021dcc710e619ea58d6;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=986b5948937cf5c5768e74447d8de7020194a75a;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr1_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr1_defs.v
index 986b59489..ed05b0e5d 100644
--- 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.