cases subpath
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)
case nil
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
hi : ∀ (h : isCons nil = true), Class.Child.class (split nil h).snd = class nil
h : isCons (cons child nil) = true
⊢ Class.Child.class (split (cons child nil) h).snd = class (cons child nil)

case cons
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
hi : ∀ (h : isCons (cons child✝ a✝) = true), Class.Child.class (split (cons child✝ a✝) h).snd = class (cons child✝ a✝)
h : isCons (cons child (cons child✝ a✝)) = true
⊢ Class.Child.class (split (cons child (cons child✝ a✝)) h).snd = class (cons child (cons child✝ a✝))