cases path <;> simp [isCons]
graph : Graph
start : Class graph
path : Path graph start
⊢ isCons path = true ↔ ∃ child subpath, path = cons child subpath
case cons
graph : Graph
start : Class graph
child✝ : Class.Child start
a✝ : Path graph (Class.Child.class child✝)
⊢ ∃ child subpath, child✝ = child ∧ HEq a✝ subpath