X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fcounters%2Frtc_ist_plus.ma;h=5156acb85e3c34bcc2a6d39b780fc3ba2e31cc17;hp=08bb3b772aa39e94a75f6eb1db13033cc8995118;hb=0bcf2dc1a27e38cb6cd3d44eb838d652926841e0;hpb=7e120a2bf2e6c0882b4f4b376c5861e001945cf4

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma
index 08bb3b772..5156acb85 100644
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist_plus.ma
@@ -33,7 +33,7 @@ lemma rtc_ist_plus_zero_dx (n) (c1) (c2): 𝐓❪n,c1❫ → 𝐓❪𝟎,c2❫ 
 /2 width=1 by rtc_ist_plus/ qed.
 
 lemma rtc_ist_succ (n) (c): 𝐓❪n,c❫ → 𝐓❪↑n,c+𝟘𝟙❫.
-#n #c #H >nplus_one_dx
+#n #c #H >nplus_unit_dx
 /2 width=1 by rtc_ist_plus/
 qed.
 
@@ -54,7 +54,7 @@ lemma rtc_ist_inv_plus_zero_dx (n) (c1) (c2): 𝐓❪n,c1 + c2❫ → 𝐓❪
 elim (rtc_ist_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct //
 qed-.
 
-lemma rtc_ist_inv_plus_one_dx:
+lemma rtc_ist_inv_plus_unit_dx:
       ∀n,c1,c2. 𝐓❪n,c1 + c2❫ → 𝐓❪𝟏,c2❫ →
       ∃∃m. 𝐓❪m,c1❫ & n = ↑m.
 #n #c1 #c2 #H #H2 destruct