cases' p with _ _ w _ huw pwv
case h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
p : Walk G u v
⊢ p ∈ {p | Walk.length p = Nat.succ n} ↔ p ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}
case h.nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
n : ℕ
⊢ Walk.nil ∈ {p | Walk.length p = Nat.succ n} ↔
    Walk.nil ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}

case h.cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
n : ℕ
w : V
huw : G.Adj u w
pwv : Walk G w v
⊢ Walk.cons huw pwv ∈ {p | Walk.length p = Nat.succ n} ↔
    Walk.cons huw pwv ∈ ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' | Walk.length p' = n}