simp [Succ, h, prefix?] at h'
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
h' : child.val ≻ path
⊢ 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
h' : nil = path
⊢ start = class path