- probe: critical bug fixed (all objects were deleted due to wrong test)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cpx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
index 3d116e292f363e9e1f8f01d1dfee3011c7d6f8b0..6e1a50a65cad82ccf0ed999097f0b4d479517819 100644 (file)
--- 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/