more on lfpx_frees.ma ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lfxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index 5c3a07a2a0de2eb1b741a642947d8231beb1be88..605af05cea8ced70374ffc829f217816f0c716e8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -26,12 +26,12 @@ definition lfxs (R) (T): relation lenv ≝
 interpretation "generic extension on referred entries (local environment)"
    'RelationStar R T L1 L2 = (lfxs R T L1 L2).
 
-definition R_confluent_lfxs: relation4 (relation3 lenv term term)
-                                       (relation3 lenv term term) … ≝
-                             λR1,R2,RP1,RP2.
-                             ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
-                             ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 →
-                             ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
+definition R_confluent2_lfxs: relation4 (relation3 lenv term term)
+                                        (relation3 lenv term term) … ≝
+                              λR1,R2,RP1,RP2.
+                              ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
+                              ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 →
+                              ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
 
 (* Basic properties ***********************************************************)