induction' p with _ x y w a p' ih
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
S : Set V
uS : u ∈ S
vS : ¬v ∈ S
⊢ ∃ e, e ∈ edges p ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
u✝ : V
uS : u✝ ∈ S
vS : ¬u✝ ∈ S
⊢ ∃ e, e ∈ edges nil ∧ e.fst ∈ S ∧ ¬e.snd ∈ S

case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
S : Set V
uS✝ : u ∈ S
vS✝ : ¬v ∈ S
x y w : V
a : G.Adj x y
p' : Walk G y w
ih : y ∈ S → ¬w ∈ S → ∃ e, e ∈ edges p' ∧ e.fst ∈ S ∧ ¬e.snd ∈ S
uS : x ∈ S
vS : ¬w ∈ S
⊢ ∃ e, e ∈ edges (cons a p') ∧ e.fst ∈ S ∧ ¬e.snd ∈ S