Theorem: SimpleGraph.Menger.Separates.symm (Untitled/Graphs/Menger.lean)

State before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : Separates G A B X
p : AB_Walk G B A
⊢ ∃ x ∈ X, x ∈ Walk.support p.to_Walk
Tactic:
simpa using h p.Reverse
State after:
no goals