case cons subpath hi => simp [extend, prefix?_cons_eq_cons_prefix? hi]
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
subpath : Path graph (Class.Child.class child✝)
hi : ∀ {leaf : Class.Child (class subpath)}, prefix? (extend subpath leaf) = some subpath
leaf : Class.Child (class (cons child✝ subpath))
⊢ prefix? (extend (cons child✝ subpath) leaf) = some (cons child✝ subpath)
no goals