X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Freq.ma;h=acfb6c4e8a4e9ea879edfee076d6d06225823844;hp=46e436d68eb2edde629e4b9d9659a114055b377f;hb=a454837a256907d2f83d42ced7be847e10361ea9;hpb=b4283c079ed7069016b8d924bbc7e08872440829

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/req.ma b/matita/matita/contribs/lambdadelta/static_2/static/req.ma
index 46e436d68..acfb6c4e8 100644
--- 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