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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_confluence.v
index afdab3d52..8b2fd4769 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr2_confluence.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr2_confluence.v
@@ -8,58 +8,57 @@ Require pr2_defs.
 
    Section pr2_confluence. (*************************************************)
 
-(* case 1.1 : pr2_pr0 pr2_pr0 ***********************************************)
+(* case 1.1 : pr2_free pr2_free *********************************************)
 
-      Remark pr2_pr0_pr0: (c:?; t0,t1,t2:?)
-                          (pr0 t0 t1) -> (pr0 t0 t2) ->
-                          (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
+      Remark pr2_free_free: (c:?; t0,t1,t2:?)
+                            (pr0 t0 t1) -> (pr0 t0 t2) ->
+                            (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
       Intros; Pr0Confluence; XEAuto.
       Qed.
 
-(* case 1.2 : pr2_pr0 pr2_delta *********************************************)
+(* case 1.2 : pr2_free pr2_delta ********************************************)
 
-      Remark pr2_pr0_delta: (c,d:?; t0,t1,t2,u:?; i:?)
-                            (pr0 t0 t1) ->
-                            (drop i (0) c (CTail d (Bind Abbr) u)) ->
-                            (subst0 i u t0 t2) ->
-                            (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
-      Intros; Pr0Subst0; XEAuto.
+      Remark pr2_free_delta: (c,d:?; t0,t1,t2,t4,u:?; i:?)
+                             (pr0 t0 t1) ->
+                             (drop i (0) c (CTail d (Bind Abbr) u)) ->
+                             (pr0 t0 t4) ->
+			     (subst0 i u t4 t2) ->
+                             (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
+      Intros; Pr0Confluence; Pr0Subst0; XEAuto.
       Qed.
 
 (* case 2.2 : pr2_delta pr2_delta *******************************************)
 
-      Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,u,u0:?; i,i0:?)
+      Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,t3,t4,u,u0:?; i,i0:?)
                               (drop i (0) c (CTail d (Bind Abbr) u)) ->
-                              (subst0 i u t0 t1) ->
+                              (pr0 t0 t3) ->
+			      (subst0 i u t3 t1) ->
                               (drop i0 (0) c (CTail d0 (Bind Abbr) u0)) ->
-                              (subst0 i0 u0 t0 t2) ->
+                              (pr0 t0 t4) ->
+			      (subst0 i0 u0 t4 t2) ->
                               (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
-      Intros.
+      Intros; Pr0Confluence; Repeat Pr0Subst0;
+      [ XEAuto | XEAuto | XEAuto | Idtac ].
       Apply (neq_eq_e i i0); Intros.
 (* case 1 : i != i0 *)
       Subst0Confluence; XEAuto.
 (* case 2 : i = i0 *)
-      Rewrite H3 in H; Rewrite H3 in H0; Clear H3 i.
-      DropDis; Inversion H1; Rewrite H5 in H0; Clear H1 H4 H5 d u.
-      Subst0Confluence; [ Rewrite H1; XEAuto | XEAuto | XEAuto | XEAuto ].
+      Rewrite H5 in H; Rewrite H5 in H3; Clear H5 i.
+      DropDis; Inversion H2; Rewrite H7 in H3; Clear H2 H6 H7 d u.
+      Subst0Confluence; [ Rewrite H2 in H0; XEAuto | XEAuto | XEAuto | XEAuto ].
       Qed.
 
 (* main *********************************************************************)
 
-      Hints Resolve pr2_pr0_pr0 pr2_pr0_delta pr2_delta_delta : ltlc.
-
-(*#* #start file *)
+      Hints Resolve pr2_free_free pr2_free_delta pr2_delta_delta : ltlc.
 
 (*#* #caption "confluence with itself: Church-Rosser property" *)
 (*#* #cap #cap c, t0, t1, t2, t *)
 
-      Theorem pr2_confluence : (c,t0,t1:?) (pr2 c t0 t1) ->
-                               (t2:?) (pr2 c t0 t2) ->
-                               (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
-
-(*#* #stop file *)
-
-      Intros; Inversion H; Inversion H0; XEAuto.
+      Theorem pr2_confluence: (c,t0,t1:?) (pr2 c t0 t1) ->
+                              (t2:?) (pr2 c t0 t2) ->
+                              (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
+      Intros; Inversion H; Inversion H0; XDEAuto 3.
       Qed.
 
    End pr2_confluence.
@@ -72,6 +71,4 @@ Require pr2_defs.
                XElim H1; Intros
             | _ -> Pr0Confluence.
 
-(*#* #start file *)
-
 (*#* #single *)