+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 →
+ ∧∧ 𝐑𝐓❪n,c1❫ & 𝐑𝐓❪n,c2❫.
+#n #c1 #c2 #H #Hc12
+elim (isrt_inv_max … H) -H #n1 #n2 #Hc1 #Hc2 #H destruct
+lapply (isrt_eq_t_trans … Hc1 … Hc12) -Hc12 #H
+<(isrt_inj … H … Hc2) -Hc2
+<idempotent_max /2 width=1 by conj/