case nil => simp [prefix?] at h
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
h : prefix? (cons child nil) = some (cons child path₂)
⊢ prefix? nil = some path₂
no goals