lemma isrt_01: ššā¦1, ššā¦.
/2 width=3 by ex1_2_intro/ qed.
+lemma isrt_eq_t_trans: ān,c1,c2. ššā¦n, c1ā¦ ā eq_t c1 c2 ā ššā¦n, c2ā¦.
+#n #c1 #c2 * #ri1 #rs1 #H destruct
+#H elim (eq_t_inv_dx ā¦ H) -H /2 width=3 by ex1_2_intro/
+qed-.
+
(* Basic inversion properties ***********************************************)
lemma isrt_inv_00: ān. ššā¦n, ššā¦ ā 0 = n.
(* Main inversion properties ************************************************)
-theorem isrt_mono: ān1,n2,c. ššā¦n1, cā¦ ā ššā¦n2, cā¦ ā n1 = n2.
+theorem isrt_inj: ān1,n2,c. ššā¦n1, cā¦ ā ššā¦n2, cā¦ ā n1 = n2.
#n1 #n2 #c * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
qed-.
+
+theorem isrt_mono: ān,c1,c2. ššā¦n, c1ā¦ ā ššā¦n, c2ā¦ ā eq_t c1 c2.
+#n #c1 #c2 * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
+qed-.