proposition: Lemma nodes_eqE x y (p q : Path x y) : (nodes p == nodes q) = (p == q).
proof: Proof. case: q p => q pth_q [p pth_p]. by rewrite !nodesE -val_eqE /= eqseq_cons eqxx. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)