case cons.nil => intro h; cases h; case _ h   => have := h.isCons; contradiction
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
no goals