+lemma s_r_to_s_rs_trans: ∀A,B,S,R. s_r_transitive A B (LTC … S) R →
+ s_rs_transitive A B S R.
+#A #B #S #R #HSR #L2 #T1 #T2 #HL2 #L1 #HT1
+elim (TC_idem … (S L1) … T1 T2)
+#_ #H @H @HSR //
+qed-.
+
+lemma s_rs_to_s_r_trans: ∀A,B,S,R. s_rs_transitive A B S R →
+ s_r_transitive A B (LTC … S) R.
+#A #B #S #R #HSR #L2 #T1 #T2 #HL2 #L1 #HT1
+elim (TC_idem … (S L1) … T1 T2)
+#H #_ @H @HSR //
+qed-.
+
+lemma s_rs_trans_TC1: ∀A,B,S,R. s_rs_transitive A B S R →
+ s_rs_transitive A B (LTC … S) R.
+#A #B #S #R #HSR #L2 #T1 #T2 #HL2 #L1 #HT1
+elim (TC_idem … (S L1) … T1 T2)
+elim (TC_idem … (S L2) … T1 T2)
+#_ #H1 #H2 #_ @H2 @HSR /3 width=3 by/
+qed-.
+