#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 →
#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 →