cases p' with
| nil => simp at h
| cons _ _ =>
  simp only [map_cons, cons.injEq] at h
  cases hinj h.1
  simp only [cons.injEq, heq_iff_eq, true_and_iff]
  apply ih
  simpa using h.2
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' : V
p : Walk G u✝¹ v✝¹
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
ih : ∀ ⦃p' : Walk G v✝ w✝⦄, Walk.map f p✝ = Walk.map f p' → p✝ = p'
p' : Walk G u✝ w✝
h : Walk.map f (cons h✝ p✝) = Walk.map f p'
⊢ cons h✝ p✝ = p'
no goals