proposition: Lemma tsorted_symconnect x y a l : TS[a, x :: l] -> x =[a]= y = (y \in x :: l) && y -[a]-> x.
proof: Proof. move=> [_ CR BR]. apply/idP/idP=> [/andP[Cxy Cyx]|/andP[yIxl Cyx]]. by rewrite (CR x y) // inE eqxx. have F := symconnect_can_to _ _ yIxl. have := BR y x yIxl Cyx. by rewrite /before /= eqxx; case: eqP => //->. Qed.
imports: mathcomp(all_ssreflect) extra