injection 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)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
h : cons child✝ w✝ = cons child✝ path₂
⊢ w✝ = path₂
no goals