cases subpath
graph : Graph
start : Class graph
child : Class.Child start
subpath subprefix : Path graph (Class.Child.class child)
h : prefix? subpath = some subprefix
⊢ prefix? (cons child subpath) = some (cons child subprefix)
case nil
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
h : prefix? nil = some subprefix
⊢ prefix? (cons child nil) = some (cons child subprefix)

case cons
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child✝ a✝) = some subprefix
⊢ prefix? (cons child (cons child✝ a✝)) = some (cons child subprefix)