X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fcounters%2Frtc_ism_plus.ma;h=4451820f9bf73a7a67758780eab3149994e6db6b;hp=5453b63fbeb436746c8b2ff5ac2cb2172ae5031b;hb=0bcf2dc1a27e38cb6cd3d44eb838d652926841e0;hpb=7e120a2bf2e6c0882b4f4b376c5861e001945cf4

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_plus.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_plus.ma
index 5453b63fb..4451820f9 100644
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ism_plus.ma
@@ -33,7 +33,7 @@ lemma rtc_ism_plus_zero_dx (n) (c1) (c2): 𝐌❪n,c1❫ → 𝐌❪𝟎,c2❫ 
 /2 width=1 by rtc_ism_plus/ qed.
 
 lemma rtc_ism_succ (n) (c): 𝐌❪n,c❫ → 𝐌❪↑n,c+𝟘𝟙❫.
-#n #c #H >nplus_one_dx
+#n #c #H >nplus_unit_dx
 /2 width=1 by rtc_ism_plus/
 qed.