X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfeq_lreq.ma;h=fc902a4a324415cdc8a867862064c16390a7bfcc;hb=88dd0e28758c693660a93ee0a9a5202c61ca09a0;hp=9021fbb75d8faa7497daf7f8806b0594c504fee8;hpb=e39d1924cd572acdf0cf8dba08f3b650dfd6abee;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lreq.ma
index 9021fbb75..fc902a4a3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lreq.ma
@@ -25,7 +25,7 @@ qed-.
 
 (* Properties with ranged equivalence for local environments ****************)
 
-lemma lreq_lfeq: ∀L1,L2,T,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → L1 ≡[f] L2 → L1 ≡[T] L2.
+lemma lreq_lfeq: ∀f,L1,L2,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f → L1 ≡[f] L2 → L1 ≡[T] L2.
 /2 width=3 by ex2_intro/ qed.
 
 (* Advanced properties ******************************************************)