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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma
index ba08f8818..6d53694c7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma
@@ -20,7 +20,7 @@ include "basic_2/dynamic/lsubv_lsubr.ma".
 (* Forward lemmas with t-bound contex-sensitive rt-computation for terms ****)
 
 (* Basic_2A1: uses: lsubsv_cprs_trans lsubsv_scpds_trans *)
-lemma lsubv_cpms_trans (a) (n) (h) (G):
-      lsub_trans … (λL. cpms h G L n) (lsubv a h G).
+lemma lsubv_cpms_trans (h) (a) (n) (G):
+      lsub_trans … (λL. cpms h G L n) (lsubv h a G).
 /3 width=6 by lsubv_fwd_lsubr, lsubr_cpms_trans/
 qed-.