exact (h' rfl).elim
case cons.tail.inr.inl.intro
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 w' : V
h' : ¬u = u
p' : Walk G x w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
ha : G.Adj u x
⊢ False
no goals