X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Flleq_llor.ma;h=df65d267a057e457dede0a2ca6afe5de45f9e377;hb=33f8507cadd3b36dc9afa227d8968dda66fe2034;hp=2a31fece3ef91b93a59ff655b972a9f9ef9c510a;hpb=598a5c56535a8339f6533227ab580aff64e2d41c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma
index 2a31fece3..df65d267a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma
@@ -13,22 +13,29 @@
 (**************************************************************************)
 
 include "basic_2/multiple/llor.ma".
+include "basic_2/multiple/llpx_sn_frees.ma".
 include "basic_2/multiple/lleq_alt.ma".
 
 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
 
-(* Properties on poinwise union for local environments **********************)
+(* Properties on pointwise union for local environments **********************)
 
-lemma llpx_sn_llor_dx: ∀R,L1,L2.
-                       (∀U,i. L2 ⊢ i ϵ 𝐅*[0]⦃U⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U⦄) →
-                       ∀T. llpx_sn R 0 T L1 L2 → ∀L. L1 ⩖[T] L2 ≡ L → L2 ≡[T, 0] L.
-#R #L1 #L2 #HR #T #H1 #L #H2
+lemma llpx_sn_llor_dx: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) →
+                       ∀L1,L2,T,d. llpx_sn R d T L1 L2 → ∀L. L1 ⩖[T, d] L2 ≡ L → L2 ≡[T, d] L.
+#R #H1R #H2R #L1 #L2 #T #d #H1 #L #H2
+lapply (llpx_sn_frees_trans … H1R H2R … H1) -H1R -H2R #HR
 elim (llpx_sn_llpx_sn_alt … H1) -H1 #HL12 #IH1
 elim H2 -H2 #_ #HL1 #IH2
 @lleq_intro_alt // #I2 #I #K2 #K #V2 #V #i #Hi #HnT #HLK2 #HLK
-lapply (ldrop_fwd_length_lt2 … HLK) #HiL
-elim (ldrop_O1_lt (Ⓕ) L1 i) // -HiL #I1 #K1 #V1 #HLK1
+lapply (drop_fwd_length_lt2 … HLK) #HiL
+elim (drop_O1_lt (Ⓕ) L1 i) // -HiL #I1 #K1 #V1 #HLK1
 elim (IH1 … HLK1 HLK2) -IH1 /2 width=1 by/ #H #_ destruct
 elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK1 -HLK2 -HLK * /2 width=1 by conj/ #H
-elim H -H /2 width=1 by/
+[ elim (ylt_yle_false … H) -H //
+| elim H -H /2 width=1 by/
+]
 qed.
+
+lemma llpx_sn_llor_dx_sym: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) →
+                           ∀L1,L2,T,d. llpx_sn R d T L1 L2 → ∀L. L1 ⩖[T, d] L2 ≡ L → L ≡[T, d] L2.
+/3 width=6 by llpx_sn_llor_dx, lleq_sym/ qed.