update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / counters / rtc_ism_plus.ma

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 5453b63fbeb436746c8b2ff5ac2cb2172ae5031b..4451820f9bf73a7a67758780eab3149994e6db6b 100644 (file)
--- 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.