proposition: Lemma unique_forestT : (forall x y, unique (fun p : Path x y => irred p)) -> is_forest [set: G].
proof: Proof. move => H x y p q [Ip _] [Iq _]. exact: H. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)