simp!
case cons.head
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
x v' w' : V
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
ha : G.Adj u v'
⊢ List.count (u, x) (edges (takeUntil (cons ha p') u (_ : List.Mem u (u :: support p')))) = 0
no goals