update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / lsubv.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
index 2ff320b82a6aa2fa4060c223d92095cd3f343d4b..6df83d988795ee7be8d9750d9ed6e280c68327b3 100644 (file)
--- 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-.