cases subpath₁
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
subpath₁ : Path graph (Class.Child.class child₁)
hi : Option.isSome (prefix? subpath₁) = true → isCons subpath₁ = true
h : Option.isSome (prefix? (cons child₁ subpath₁)) = true
⊢ isCons (cons child₁ subpath₁) = true
case nil
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : Option.isSome (prefix? nil) = true → isCons nil = true
h : Option.isSome (prefix? (cons child₁ nil)) = true
⊢ isCons (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 : Option.isSome (prefix? (cons child✝ a✝)) = true → isCons (cons child✝ a✝) = true
h : Option.isSome (prefix? (cons child₁ (cons child✝ a✝))) = true
⊢ isCons (cons child₁ (cons child✝ a✝)) = true