X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Flsubv_lsubv.ma;h=0108c016328eac68c593c2b291fc7e76c593e25a;hb=ba7b8553850e4a33cf8607b07758392230d9ed40;hp=d416b5f40fb4d55177c64fa7530a1871118e8c88;hpb=c0d38a82464481e3c8fd68e4b00d7b9b448df462;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubv.ma
index d416b5f40..0108c0163 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubv.ma
@@ -19,8 +19,8 @@ include "basic_2/dynamic/lsubv_cnv.ma".
 (* Main properties **********************************************************)
 
 (* Note: not valid in Basic_2A1 *)
-theorem lsubv_trans (a) (h) (G): Transitive … (lsubv a h G).
-#a #h #G #L1 #L #H elim H -L1 -L //
+theorem lsubv_trans (h) (a) (G): Transitive … (lsubv h a G).
+#h #a #G #L1 #L #H elim H -L1 -L //
 [ #I #K1 #K #HK1 #IH #Y #H
   elim (lsubv_inv_bind_sn … H) -H *
   [ #K2 #HK2 #H destruct /3 width=1 by lsubv_bind/