proposition: Lemma link_unique_lift (x y : link) : unique (fun p : Path x y => irred p /\ None \notin p).
proof: Proof. move: x y => [x|] [y|] p q [Ip Np] [Iq Nq]; try by rewrite ?(@path_end link) ?(@path_begin link) in Np Nq. gen have H,Hp : p Ip Np / {subset p <= codom Some}. { move => [u|]; by rewrite ?codom_f // (negbTE Np). } case: (lift_Path (p' := p)) => //. case: (lift_Path (p' := q)) => //; first exact: H. move => p0 Ep Ip0 q0 Eq Iq0. have E : p0 = q0. apply: forestP; by rewrite ?Ip0 ?Iq0. apply/eqP. rewrite -nodes_eqE. by apply/eqP;congruence. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)