milestone update in ground

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

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 ed5669cc9ce62713bfeefaebc13b315817442414..65f22c2d68b6c8d8fe27eca5c5cbdfd86fe37668 100644 (file)
--- 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.