split_ifs with h''
case cons.tail.inr
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 u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
h' : ¬u' = u
⊢ (if (u, x) = (u', v') then Nat.succ (List.count (u, x) (edges (takeUntil p' u (_ : u ∈ support p'))))
    else List.count (u, x) (edges (takeUntil p' u (_ : u ∈ support p')))) =
    0
case cons.tail.inr.inl
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 u' v' w' : V
ha : G.Adj u' v'
p' : Walk G v' w'
ih : ∀ (h : u ∈ support p'), List.count (u, x) (edges (takeUntil p' u h)) = 0
a✝ : List.Mem u (support p')
h' : ¬u' = u
h'' : (u, x) = (u', v')
⊢ False

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