exists ‹_›, ‹_›
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
case cons
graph : Graph
start : Class graph
child✝ : Class.Child start
a✝ : Path graph (Class.Child.class child✝)
⊢ child✝ = child✝ ∧ HEq a✝ a✝