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âŦ.
+lemma isrt_eq_t_trans: ân,c1,c2. ððâŠn,c1âŦ â rtc_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/
+#H elim (rtc_eq_t_inv_dx âĶ H) -H /2 width=3 by ex1_2_intro/
qed-.
(* Basic inversion properties ***********************************************)
#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.
+theorem isrt_mono: ân,c1,c2. ððâŠn,c1âŦ â ððâŠn,c2âŦ â rtc_eq_t c1 c2.
#n #c1 #c2 * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
qed-.