cases subpath₁
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
subpath₁ : Path graph (Class.Child.class child₁)
hi : isCons subpath₁ = true → Option.isSome (prefix? subpath₁) = true
h : isCons (cons child₁ subpath₁) = true
⊢ Option.isSome (prefix? (cons child₁ subpath₁)) = true
case nil
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : isCons nil = true → Option.isSome (prefix? nil) = true
h : isCons (cons child₁ nil) = true
⊢ Option.isSome (prefix? (cons child₁ nil)) = true

case cons
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
child✝ : Class.Child (Class.Child.class child₁)
a✝ : Path graph (Class.Child.class child✝)
hi : isCons (cons child✝ a✝) = true → Option.isSome (prefix? (cons child✝ a✝)) = true
h : isCons (cons child₁ (cons child✝ a✝)) = true
⊢ Option.isSome (prefix? (cons child₁ (cons child✝ a✝))) = true