X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfeq_lfeq.ma;h=602c5868561dd0d339048b563513bf655d41ebb5;hb=e9da8e091898b6e67a2f270581bdc5cdbe80e9b0;hp=a6f564763d69cafd72c5daf3da81bb9709800150;hpb=3a430d712f9d87185e9271b7b0c5188c5f311e4b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma
index a6f564763..602c58685 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma
@@ -21,7 +21,7 @@ include "basic_2/static/lfeq_lreq.ma".
 
 (* Main properties **********************************************************)
 
-theorem lfeq_bind: ∀I,L1,L2,V1,V2,T,p.
+theorem lfeq_bind: ∀p,I,L1,L2,V1,V2,T.
                    L1 ≡[V1] L2 → L1.ⓑ{I}V1 ≡[T] L2.ⓑ{I}V2 →
                    L1 ≡[ⓑ{p,I}V1.T] L2.
 /2 width=2 by lfxs_bind/ qed.