+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/