more additions and corrections for the article

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

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/req.ma b/matita/matita/contribs/lambdadelta/static_2/static/req.ma
index 46e436d68eb2edde629e4b9d9659a114055b377f..acfb6c4e8a4e9ea879edfee076d6d06225823844 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/req.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/req.ma
@@ -76,8 +76,8 @@ qed-.
 
 (* Basic_properties *********************************************************)
 
-lemma frees_req_conf: ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≘ f →
-                      ∀L2. L1 ≡[T] L2 → L2 ⊢ 𝐅*⦃T⦄ ≘ f.
+lemma frees_req_conf: ∀f,L1,T. L1 ⊢ 𝐅+⦃T⦄ ≘ f →
+                      ∀L2. L1 ≡[T] L2 → L2 ⊢ 𝐅+⦃T⦄ ≘ f.
 #f #L1 #T #H elim H -f -L1 -T
 [ /2 width=3 by frees_sort/
 | #f #i #Hf #L2 #H2