advances towards confluence of reduction in local environments ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lfeq_lfeq.ma

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 a6f564763d69cafd72c5daf3da81bb9709800150..677f53973585f56aa2be1b980877a53e12128936 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "basic_2/relocation/lreq_lreq.ma".
-include "basic_2/static/frees_frees.ma".
 include "basic_2/static/lfxs_lfxs.ma".
 include "basic_2/static/lfeq_lreq.ma".
 
@@ -21,7 +20,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.