proposition: Lemma link_unique_None (x : link) : unique (fun p : @Path link None x => irred p).
proof: Proof. move: x => [x|] p q Ip Iq; last by rewrite (irredxx Ip) (irredxx Iq). case: (splitL p) => // [] [y|] [/= xy] [p'] [P1 _] //. case: (splitL q) => // [] [z|] [/= xz] [q'] [Q1 _] //. subst. move: Ip Iq. rewrite !irred_edgeL => /andP[Np Ip] /andP[Nq Iq]. have ? : y = z. { apply: (link_bypass (p := pcat p' (prev q'))) => //. by rewrite (@mem_pcat link) mem_prev negb_or Np Nq. } subst. congr pcat; first exact: val_inj. exact: link_unique_lift. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)