cases path₁ <;> cases path₂
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ path₁ ≂ path₂ → prefix? path₁ = prefix? path₂
case nil.nil
graph✝ : Graph
a✝ : Class graph✝
⊢ Path.nil ≂ Path.nil → prefix? Path.nil = prefix? Path.nil

case nil.cons
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.nil ≂ Path.cons child✝ a✝ → prefix? Path.nil = prefix? (Path.cons child✝ a✝)

case cons.nil
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝ a✝ ≂ Path.nil → prefix? (Path.cons child✝ a✝) = prefix? Path.nil

case cons.cons
graph✝ : Graph
a✝² : Class graph✝
child✝¹ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝²
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝¹ a✝¹ ≂ Path.cons child✝ a✝ → prefix? (Path.cons child✝¹ a✝¹) = prefix? (Path.cons child✝ a✝)