X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fsteps%2Frtc_isrt_max.ma;h=ed314bb2239840780632d219180f462d38628271;hp=27b5d84f3485973804b846faf1cce03366bdc39f;hb=3c7b4071a9ac096b02334c1d47468776b948e2de;hpb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea

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 27b5d84f3..ed314bb22 100644
--- 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