simp [hs, prefix?] at h ⊢
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
⊢ prefix? (cons child subpath) = some path₂
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
h :
  (do
      let x ← some w✝
      some (cons child✝ x)) =
    some (cons child✝ path₂)
⊢ w✝ = path₂