(**************************************************************************)
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 **********************)
-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
elim (ldrop_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.