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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
index 04b4044be..ece33413e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
@@ -19,10 +19,10 @@ include "basic_2/static/lfxs.ma".
 
 (* Main properties ******************************************************)
 
-theorem lfxs_bind: ∀R,I,L1,L2,V1,V2,T,p.
+theorem lfxs_bind: ∀R,p,I,L1,L2,V1,V2,T.
                    L1 ⦻*[R, V1] L2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2 →
                    L1 ⦻*[R, ⓑ{p,I}V1.T] L2.
-#R #I #L1 #L2 #V1 #V2 #T #p * #f1 #HV #Hf1 * #f2 #HT #Hf2
+#R #p #I #L1 #L2 #V1 #V2 #T * #f1 #HV #Hf1 * #f2 #HT #Hf2
 elim (lexs_fwd_pair … Hf2) -Hf2 #Hf2 #_ elim (sor_isfin_ex f1 (⫱f2))
 /3 width=7 by frees_fwd_isfin, frees_bind, lexs_join, isfin_tl, ex2_intro/
 qed.