milestone update in basic_2, update in ground and static_2

[helm.git] / matita / matita / contribs / lambdadelta / ground / steps / rtc_isrt_max.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_max.ma b/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_max.ma
index 27b5d84f3485973804b846faf1cce03366bdc39f..ed314bb2239840780632d219180f462d38628271 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_max.ma
+++ b/matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt_max.ma
@@ -58,7 +58,7 @@ elim (isrt_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
 lapply (isrt_inj … Hn2 H2) -c2 #H destruct //
 qed-.
 
-lemma isrt_inv_max_eq_t: ∀n,c1,c2. 𝐑𝐓❪n,c1 ∨ c2❫ → eq_t c1 c2 →
+lemma isrt_inv_max_eq_t: ∀n,c1,c2. 𝐑𝐓❪n,c1 ∨ c2❫ → rtc_eq_t c1 c2 →
                          ∧∧ 𝐑𝐓❪n,c1❫ & 𝐑𝐓❪n,c2❫.
 #n #c1 #c2 #H #Hc12
 elim (isrt_inv_max … H) -H #n1 #n2 #Hc1 #Hc2 #H destruct