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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma
index c02ec80b0..aad53743d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma
@@ -20,6 +20,6 @@ include "basic_2/dynamic/lsubv_lsubr.ma".
 (* Forward lemmas with context-sensitive r-equivalence for terms ************)
 
 (* Basic_2A1: uses: lsubsv_cprs_trans *)
-lemma lsubv_cpcs_trans (a) (h) (G): lsub_trans … (cpcs h G) (lsubv a h G).
+lemma lsubv_cpcs_trans (h) (a) (G): lsub_trans … (cpcs h G) (lsubv h a G).
 /3 width=6 by lsubv_fwd_lsubr, lsubr_cpcs_trans/
 qed-.