intro h
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
⊢ child.val = cons c nil → start = class path
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
⊢ start = class path