induction path
graph : Graph
start : Class graph
path : Path graph start
h : Option.isSome (prefix? path) = true
⊢ isCons path = true
case nil
graph : Graph
start x✝ : Class graph
h : Option.isSome (prefix? nil) = true
⊢ isCons nil = true

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