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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v
index 2267e88ae..6f5019bc9 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v
@@ -3,24 +3,23 @@ Require pr3_defs.
 
    Section pr3_confluence. (*************************************************)
 
+(*#* #stop theorem *)
+
 (*#* #caption "confluence with single step reduction: strip lemma" *)
 (*#* #cap #cap c, t0, t1, t2, t *)
 
       Theorem pr3_strip : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr2 c t0 t2) ->
                           (EX t | (pr3 c t1 t) & (pr3 c t2 t)).
-
-(*#* #stop proof *)
-
       Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1 : pr3_refl *)
       XEAuto.
-(* case 2 : pr3_u *)
+(* case 2 : pr3_sing *)
       Pr2Confluence.
       LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
       XElim H1; Intros; XEAuto.
       Qed.
 
-(*#* #start proof *)
+(*#* #start theorem *)
 
 (*#* #caption "confluence with itself: Church-Rosser property" *)
 (*#* #cap #cap c, t0, t1, t2, t *)
@@ -31,9 +30,9 @@ Require pr3_defs.
 (*#* #stop file *)
 
       Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1 : pr3_refl *)
       XEAuto.
-(* case 2 : pr3_u *)
+(* case 2 : pr3_sing *)
       LApply (pr3_strip c t3 t5); [ Clear H2; Intros H2 | XAuto ].
       LApply (H2 t2); [ Clear H H2; Intros H | XAuto ].
       XElim H; Intros.