-lemma eq_t_inv_dx: ∀ri1,rs1,ti,ts,y. eq_t (〈ri1,rs1,ti,ts〉) y →
- ∃∃ri2,rs2. y = 〈ri2,rs2,ti,ts〉.
-/2 width=5 by eq_t_inv_dx_aux/ qed-.
+lemma rtc_eq_t_inv_dx:
+ ∀ri1,rs1,ti,ts,y. rtc_eq_t (〈ri1,rs1,ti,ts〉) y →
+ ∃∃ri2,rs2. y = 〈ri2,rs2,ti,ts〉.
+/2 width=5 by rtc_eq_t_inv_dx_aux/ qed-.