rw [suffix]
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ class (suffix path h) = class path
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ class
      (match path, h with
      | nil, h => Bool.noConfusion h
      | cons child subpath, h => subpath) =
    class path