split_ifs with h'
case cons.tail
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')
⊢ List.count (u, x)
      (edges
        (if h : u' = u then
          Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u)
            (_ : List.Mem u (u' :: support p'))
        else cons ha (takeUntil p' u (_ : u ∈ support p')))) =
    0
case cons.tail.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
⊢ List.count (u, x)
      (edges
        (Eq.rec (motive := fun x x_1 => x ∈ u' :: support p' → Walk G u' x) (fun h => nil) (_ : u' = u)
          (_ : List.Mem u (u' :: support p')))) =
    0

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
⊢ List.count (u, x) (edges (cons ha (takeUntil p' u (_ : u ∈ support p')))) = 0