simp [getVert, hxy]
case cons.zero
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ {i : ℕ}, i < length p✝ → G.Adj (getVert p✝ i) (getVert p✝ (i + 1))
hi : Nat.zero < length (cons hxy p✝)
⊢ G.Adj (getVert (cons hxy p✝) Nat.zero) (getVert (cons hxy p✝) (Nat.zero + 1))
no goals