cases h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h' : G.Adj u v✝
p' : Walk G v✝ v
e : V × V
h : e ∈ edges (cons h' p')
⊢ e ∈ edgeSet G
case head
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h' : G.Adj u v✝
p' : Walk G v✝ v
⊢ (u, v✝) ∈ edgeSet G

case tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v v✝ : V
h' : G.Adj u v✝
p' : Walk G v✝ v
e : V × V
a✝ : List.Mem e (edges p')
⊢ e ∈ edgeSet G