update in lambdadelta

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / lsuba.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsuba.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsuba.ma
index fd30febbfd87fad44df62d014812710f261653a0..54b6aa1cb3b8418d71d90c7aae89e4bb1ad5149c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/lsuba.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/lsuba.ma
@@ -67,7 +67,7 @@ fact lsuba_inv_atom2_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → L2 = ⋆ → L1 = 
 ]
 qed-.
 
-lemma lsubc_inv_atom2: ∀G,L1. G ⊢ L1 ⫃⁝ ⋆ → L1 = ⋆.
+lemma lsuba_inv_atom2: ∀G,L1. G ⊢ L1 ⫃⁝ ⋆ → L1 = ⋆.
 /2 width=4 by lsuba_inv_atom2_aux/ qed-.
 
 fact lsuba_inv_bind2_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀I,K2. L2 = K2.ⓘ[I] →