X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flexs_lexs.ma;h=c0d7c6a1298098ea1078133c59e8ccc52fc31656;hb=b4b5f03ffca4f250a1dc02f277b70e4f33ac8a9b;hp=91dc222975f7defbd3a3995f8d0cf5649cf49023;hpb=4b1dee70d9f24b47ab1f93cf1e63862b7b71a645;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
index 91dc22297..c0d7c6a12 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
@@ -13,8 +13,6 @@
 (**************************************************************************)
 
 include "ground_2/relocation/rtmap_sand.ma".
-include "ground_2/relocation/rtmap_sor.ma".
-include "basic_2/relocation/lexs.ma".
 include "basic_2/relocation/drops.ma".
 
 (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
@@ -45,8 +43,8 @@ theorem lexs_trans (RN) (RP) (f): lexs_transitive RN RN RN RN RP →
 (* Basic_2A1: includes: lpx_sn_conf *)
 theorem lexs_conf (RN1) (RP1) (RN2) (RP2):
                   ∀L,f.
-                  (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V →  ⫱*[n] f = ⫯g → lexs_pw_confluent2_R RN1 RN2 RN1 RP1 RN2 RP2 g K V) →
-                  (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V →  ⫱*[n] f = ↑g → lexs_pw_confluent2_R RP1 RP2 RN1 RP1 RN2 RP2 g K V) →
+                  (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ⫯g = ⫱*[n] f → R_pw_confluent2_lexs RN1 RN2 RN1 RP1 RN2 RP2 g K V) →
+                  (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ↑g = ⫱*[n] f → R_pw_confluent2_lexs RP1 RP2 RN1 RP1 RN2 RP2 g K V) →
                   pw_confluent2 … (lexs RN1 RP1 f) (lexs RN2 RP2 f) L.
 #RN1 #RP1 #RN2 #RP2 #L elim L -L
 [ #f #_ #_ #L1 #H1 #L2 #H2 >(lexs_inv_atom1 … H1) >(lexs_inv_atom1 … H2) -H2 -H1