X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Flsubv.ma;h=6df83d988795ee7be8d9750d9ed6e280c68327b3;hp=2ff320b82a6aa2fa4060c223d92095cd3f343d4b;hb=21e6d5cb0c9b6d6a6b9975b78ae752120a969cd6;hpb=48bd1f41417fb167a100eb1613a64a711484b69a

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
index 2ff320b82..6df83d988 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
@@ -74,7 +74,7 @@ fact lsubv_inv_atom_dx_aux (h) (a) (G):
 qed-.
 
 (* Basic_2A1: uses: lsubsv_inv_atom2 *)
-lemma lsubv_inv_atom2 (h) (a) (G):
+lemma lsubv_inv_atom_dx (h) (a) (G):
       ∀L1. G ⊢ L1 ⫃![h,a] ⋆ → L1 = ⋆.
 /2 width=6 by lsubv_inv_atom_dx_aux/ qed-.