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

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubf_frees.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubf_frees.ma
index 713f79c7d..963893a24 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/lsubf_frees.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubf_frees.ma
@@ -18,8 +18,9 @@ include "static_2/static/lsubf.ma".
 
 (* Properties with context-sensitive free variables *************************)
 
-lemma lsubf_frees_trans: ∀f2,L2,T. L2 ⊢ 𝐅*⦃T⦄ ≘ f2 →
-                         ∀f1,L1. ⦃L1,f1⦄ ⫃𝐅* ⦃L2,f2⦄ → L1 ⊢ 𝐅*⦃T⦄ ≘ f1.
+lemma lsubf_frees_trans:
+      ∀f2,L2,T. L2 ⊢ 𝐅+⦃T⦄ ≘ f2 →
+      ∀f1,L1. ⦃L1,f1⦄ ⫃𝐅+ ⦃L2,f2⦄ → L1 ⊢ 𝐅+⦃T⦄ ≘ f1.
 #f2 #L2 #T #H elim H -f2 -L2 -T
 [ /3 width=5 by lsubf_fwd_isid_dx, frees_sort/
 | #f2 #i #Hf2 #g1 #Y1 #H