split_ifs with h' <;> subst_vars <;> simp [*]
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 u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
a✝ : List.Mem u (support p✝)
⊢ append
      (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 h✝ (takeUntil p✝ u (_ : u ∈ support p✝)))
      (if h : u✝ = u then
        Eq.rec (motive := fun x x_1 => x ∈ u✝ :: support p✝ → Walk G x w✝) (fun h => cons h✝ p✝) (_ : u✝ = u)
          (_ : List.Mem u (u✝ :: support p✝))
      else dropUntil p✝ u (_ : u ∈ support p✝)) =
    cons h✝ p✝
no goals