some advances on pointwise union for local environments ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / lpx_sn_alt.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma
index b5aa43cf8e6279f3d97c95e2e9c975519ae59a35..c9c381a32b300fc7456b6736ea4d4a662216450b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma
@@ -137,7 +137,7 @@ qed.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma lpx_sn_inv_alt: ∀R,L1,L2. lpx_sn R L1 L2 →
+lemma lpx_sn_inv_gen: ∀R,L1,L2. lpx_sn R L1 L2 →
                       |L1| = |L2| ∧
                       ∀I1,I2,K1,K2,V1,V2,i.
                       ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →