X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfxs_lfxs.ma;h=4cf5505ccbce0d2aa2a09af987392592d932b7ba;hb=7632da8aa4f6751e351546be3d90fb23f634108c;hp=78b1c526b359932c807b480cd7f903a91e6396ec;hpb=d4ab51c20dbccd1e88cd2c4dcdaf3b4e56301155;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
index 78b1c526b..4cf5505cc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
@@ -70,6 +70,25 @@ elim (HR … Hf … H) -HR -Hf -H
 /4 width=7 by sle_lexs_trans, ex2_intro/
 qed-.
 
+lemma lfxs_bind_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
+                          lexs_frees_confluent … R1 cfull →
+                          ∀I,L1,L2,V1,T. L1.ⓑ{I}V1 ⦻*[R1, T] L2 → ∀p.
+                          ∃∃L,V. L1 ⦻*[R1, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ⦻*[R2, T] L2 & R1 L1 V1 V.
+#R1 #R2 #HR1 #HR2 #HR #I #L1 #L2 #V1 #T * #f #Hf #HL12 #p
+elim (frees_total L1 (ⓑ{p,I}V1.T)) #g #Hg
+elim (frees_inv_bind … Hg) #y1 #y2 #_ #H #Hy
+lapply(frees_mono … H … Hf) -H #H2
+lapply (tl_eq_repl … H2) -H2 #H2
+lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
+lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
+lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg
+elim (lexs_sle_split … HR1 HR2 … HL12 … Hfg) -HL12 #Y #H #HL2
+lapply (sle_lexs_trans … H … Hfg) // #H0
+elim (lexs_inv_next1 … H) -H #L #V #HL1 #HV0 #H destruct
+elim (HR … Hf … H0) -HR -Hf -H0
+/4 width=7 by sle_lexs_trans, ex3_2_intro, ex2_intro/
+qed-.
+
 (* Main properties **********************************************************)
 
 (* Basic_2A1: uses: llpx_sn_bind llpx_sn_bind_O *)