induction path
graph : Graph
start : Class graph
path : Path graph start
leaf : Class.Child (class path)
⊢ prefix? (extend path leaf) = some path
case nil
graph : Graph
start x✝ : Class graph
leaf : Class.Child (class nil)
⊢ prefix? (extend nil leaf) = some nil

case cons
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
a✝ : Path graph (Class.Child.class child✝)
a_ih✝ : ∀ {leaf : Class.Child (class a✝)}, prefix? (extend a✝ leaf) = some a✝
leaf : Class.Child (class (cons child✝ a✝))
⊢ prefix? (extend (cons child✝ a✝) leaf) = some (cons child✝ a✝)