∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v w : V} (h : G.Adj u v)
  (p : G.Walk v w),
  ((SimpleGraph.Walk.map f p).IsPath → p.IsPath) →
    (SimpleGraph.Walk.map f (SimpleGraph.Walk.cons h p)).IsPath → (SimpleGraph.Walk.cons h p).IsPath