case cons child subpath hi =>
  cases subpath
  case nil => rfl
  case cons child' subpath => rw [split]; exact hi h
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
subpath : Path graph (Class.Child.class child)
hi : ∀ (h : isCons subpath = true), Class.Child.class (split subpath h).snd = class subpath
h : isCons (cons child subpath) = true
⊢ Class.Child.class (split (cons child subpath) h).snd = class (cons child subpath)
no goals