X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fsteps%2Frtc_plus.ma;h=49ce55082238d18d774b43970648fd2f0c457321;hb=397413c4196f84c81d61ba7dd79b54ab1c428ebb;hp=ad9a04f01171bfb1def1287d4947d0bdc4ca83cb;hpb=24ba1bb3f67505d3e384747ff90d26d3996bd3f5;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
index ad9a04f01..49ce55082 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma
@@ -68,7 +68,7 @@ lemma isrt_plus_O2: ân,c1,c2. ððâ¦n, c1â¦ â ððâ¦0, c2â¦ â
 #n #c1 #c2 #H1 #H2 >(plus_n_O n) /2 width=1 by isrt_plus/
 qed.
 
-lemma isrt_succ: ân,c. ððâ¦n, câ¦ â ððâ¦â«¯n, c+ððâ¦.
+lemma isrt_succ: ân,c. ððâ¦n, câ¦ â ððâ¦ân, c+ððâ¦.
 /2 width=1 by isrt_plus/ qed.
 
 (* Inversion properties with test for constrained rt-transition counter *****)
@@ -87,7 +87,7 @@ lapply (isrt_inj â¦ Hn2 H2) -c2 #H destruct //
 qed-.
 
 lemma isrt_inv_plus_SO_dx: ân,c1,c2. ððâ¦n, c1 + c2â¦ â ððâ¦1, c2â¦ â
-                           ââm. ððâ¦m, c1â¦ & n = â«¯m.
+                           ââm. ððâ¦m, c1â¦ & n = âm.
 #n #c1 #c2 #H #H2
 elim (isrt_inv_plus â¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
 lapply (isrt_inj â¦ Hn2 H2) -c2 #H destruct