rw [split]
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))
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
      (match split (cons child' subpath) (_ : isCons (cons child' subpath) = true) with
        | { fst := sub, snd := cls } => { fst := cons child sub, snd := cls }).snd =
    class (cons child (cons child' subpath))