cases h : (Path.cons child path₁).prefix?
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
case none
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h : prefix? (Path.cons child path₁) = none
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂

case some
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
val✝ : Path graph✝ cls✝
h : prefix? (Path.cons child path₁) = some val✝
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂