simp only [edges_cons, support_cons, List.nodup_cons] at h ⊢
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : List.Nodup (support p') → List.Nodup (edges p')
h : List.Nodup (support (cons h✝ p'))
⊢ List.Nodup (edges (cons h✝ p'))
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : List.Nodup (support p') → List.Nodup (edges p')
h : ¬u✝ ∈ support p' ∧ List.Nodup (support p')
⊢ ¬(u✝, v✝) ∈ edges p' ∧ List.Nodup (edges p')