- notation for the exclusion binder in local envirinments

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lfxs_lfxs.ma

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 78b1c526b359932c807b480cd7f903a91e6396ec..4cf5505ccbce0d2aa2a09af987392592d932b7ba 100644 (file)
--- 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 *)