theorem Graph.IsWalk.isWalk_or_isWalk_compl_of_closedSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList α β} (H : G.ClosedSubgraph) (hW : G.IsWalk W) : (↑H).IsWalk W ∨ (↑Hᶜ).IsWalk W

theorem Graph.ConnBetween.mem_vertexSet_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (H : G.ClosedSubgraph) {x y : α} : G.ConnBetween x y → (x ∈ (↑H).vertexSet ↔ y ∈ (↑H).vertexSet)

theorem Graph.IsWalk.isWalk_or_isWalk_of_union_of_disjoint {α : Type u_1} {β : Type u_2} {G H : Graph α β} {W : WList α β} (h : G.StronglyDisjoint H) (hW : (G ∪ H).IsWalk W) : G.IsWalk W ∨ H.IsWalk W

theorem Graph.IsWalk.prefixUntil_isWalk_subgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList α β} {H : G.Subgraph} [DecidablePred fun (x : α) => x ∈ (↑Hᶜ).vertexSet] (hW : G.IsWalk W) (hWf : W.first ∈ (↑H).vertexSet) : (↑H).IsWalk (W.prefixUntil fun (x : α) => x ∈ (↑Hᶜ).vertexSet)

theorem Graph.IsSimpleficationOf.connBetween_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {x y : α} (h : G.IsSimpleficationOf H) : G.ConnBetween x y ↔ H.ConnBetween x y