]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma
update in static_2 and basic_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / lsubv_cpcs.ma
index c02ec80b0f55354043d35505678840c2bd0748a1..aad53743d8e9394dc34746655ce5148adc1fdfa1 100644 (file)
@@ -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-.