proposition: Lemma pathS_eta (p : pathS) : p = @PathS (fst p) (lst p) (tagged p).
proof: Proof. by case: p => [[x y] ri]. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)