proposition: Lemma forestP (T : forest) (x y : T) (p q : Path x y) : irred p -> irred q -> p = q.
proof: Proof. move/forestT_unique : (@forest_is_forest T) => fP. move => Ip Iq. exact: fP. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)