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