X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fcounters%2Frtc_max_shift.ma;h=65f22c2d68b6c8d8fe27eca5c5cbdfd86fe37668;hb=55c768d7e45babb300b5010463ba3196a68f1bbe;hp=ed5669cc9ce62713bfeefaebc13b315817442414;hpb=15212e44902f25536f6e2de4bec4cedcd9a9804d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_max_shift.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_max_shift.ma
index ed5669cc9..65f22c2d6 100644
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_max_shift.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_max_shift.ma
@@ -21,6 +21,6 @@ include "ground/counters/rtc_max.ma".
 
 lemma rtc_max_shift (c1) (c2): ((↕*c1) ∨ (↕*c2)) = ↕*(c1∨c2).
 * #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
-<rtc_shift_rew <rtc_shift_rew <rtc_shift_rew <rtc_max_rew
+<rtc_shift_unfold <rtc_shift_unfold <rtc_shift_unfold <rtc_max_unfold
 <nmax_assoc <nmax_assoc <nmax_assoc <nmax_assoc //
 qed.