proposition: Lemma mem_del_edge_liftS (G : diGraph) (a b : G) (p : pathS (del_edge a b)) x : (x \in del_edge_liftS p) = (x \in p).
proof: Proof. by case: p => [[u v] p]. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)