more on lfpx_frees.ma ...

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma
index 3d6a2658e038b91b2f6eedc35a330705d4f428dc..444d413ef4230f151039777d22a60aa2bd10f6a6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma
@@ -22,7 +22,7 @@ axiom frees_lexs_conf_sle: ∀RN,RP,f1,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 →
                            ∀L2. L1 ⦻*[RN, RP, f1] L2 →
                            ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1.
 
-theorem lfxs_conf: ∀R. R_confluent_lfxs R R R R →
+theorem lfxs_conf: ∀R. R_confluent2_lfxs R R R R →
                    ∀T. confluent … (lfxs R T).
 #R #H1R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02
 lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12
@@ -47,4 +47,4 @@ lemma pippo: ∀R1,R2,RP1,RP2. R_confluent_lfxs R1 R2 RP1 RP2 →
              lexs_confluent R1 R2 RP1 cfull RP2 cfull.
 #R1 #R2 #RP1 #RP2 #HR #f #L0 #T0 #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2
 #HL02
-*)
\ No newline at end of file
+*)