X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcpx.ma;h=6e1a50a65cad82ccf0ed999097f0b4d479517819;hb=ebc33b6d5b68400bc8411973ed4c9ed50d0c52a6;hp=3d116e292f363e9e1f8f01d1dfee3011c7d6f8b0;hpb=65008df95049eb835941ffea1aa682c9253c4c2b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
index 3d116e292..6e1a50a65 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
@@ -49,12 +49,12 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma lsubx_cpx_trans: ∀h,g. lsub_trans … (cpx h g) lsubx.
+lemma lsubr_cpx_trans: ∀h,g. lsub_trans … (cpx h g) lsubr.
 #h #g #L1 #T1 #T2 #H elim H -L1 -T1 -T2
 [ //
 | /2 width=2/
 | #I #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (lsubx_fwd_ldrop2_bind … HL12 … HLK1) -HL12 -HLK1 *
+  elim (lsubr_fwd_ldrop2_bind … HL12 … HLK1) -HL12 -HLK1 *
   [ /3 width=7/ | /4 width=7/ ]
 |4,9: /4 width=1/
 |5,7,8: /3 width=1/