X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fsteps%2Frtc_max.ma;h=471f2d6ba10baa7fe1ad0f614a3970e6a1cd4d5c;hb=a09b60bd574adf1a7d3e423023009cb20c79d449;hp=46f457536456d6e034d544f3e4c1e604101bb6e0;hpb=89ea663d91904f483f8248cfaeaed5eda8715da2;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma
index 46f457536..471f2d6ba 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma
@@ -71,6 +71,10 @@ lemma isrt_max_O2: ân,c1,c2. ððâ¦n, c1â¦ â ððâ¦0, c2â¦ â 
 #n #c1 #c2 #H1 #H2 >(max_O2 n) /2 width=1 by isrt_max/
 qed.
 
+lemma isrt_max_idem1: ân,c1,c2. ððâ¦n, c1â¦ â ððâ¦n, c2â¦ â ððâ¦n, c1â¨c2â¦.
+#n #c1 #c2 #H1 #H2 >(idempotent_max n) /2 width=1 by isrt_max/
+qed.
+
 (* Inversion properties with test for constrained rt-transition counter *****)
 
 lemma isrt_inv_max: ân,c1,c2. ððâ¦n, c1 â¨ c2â¦ â
@@ -83,7 +87,7 @@ qed-.
 lemma isrt_inv_max_O_dx: ân,c1,c2. ððâ¦n, c1 â¨ c2â¦ â ððâ¦0, c2â¦ â ððâ¦n, c1â¦.
 #n #c1 #c2 #H #H2
 elim (isrt_inv_max â¦ H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
-lapply (isrt_mono â¦ Hn2 H2) -c2 #H destruct //
+lapply (isrt_inj â¦ Hn2 H2) -c2 #H destruct //
 qed-.
 
 (* Properties with shift ****************************************************)