proposition: Lemma link_bypass (x y : T) (p : @Path link (Some x) (Some y)) : x \in U -> y \in U -> None \notin p -> x = y.
proof: Proof. move => xU yU Np. case: (lift_Path (p' := p)) => // => [|p' _ _]. { move => [u|]; by rewrite ?codom_f // (negbTE Np). } apply: contraTeq isT => /U_disc => /(_ xU yU). by rewrite (Path_connect p'). Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)