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