exact Or.inr (edges_fst_mem_support_of_mem_darts _ hd)
case inr
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
d : V × V
hd : d ∈ edges p'
⊢ d.fst = u ∨ d.fst ∈ support p'
no goals