-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