case _ h _ => have := h.isCons; contradiction
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
h : Path.nil ≻ parent✝
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝¹)
no goals