cases h
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✝)
h : Path.cons child✝¹ a✝¹ ≂ Path.cons child✝ a✝
⊢ prefix? (Path.cons child✝¹ a✝¹) = prefix? (Path.cons child✝ a✝)
case 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✝)
parent✝ : Path graph✝ a✝⁴
a✝¹ : Path.cons child✝¹ a✝³ ≻ parent✝
a✝ : Path.cons child✝ a✝² ≻ parent✝
⊢ prefix? (Path.cons child✝¹ a✝³) = prefix? (Path.cons child✝ a✝²)