case mp =>
  cases path₁ <;> cases path₂
  case nil.nil => simp
  case cons.cons => intro h; cases h; simp_all [Succ]
  case nil.cons => intro h; cases h; case _ h _ => have := h.isCons; contradiction
  case cons.nil => intro h; cases h; case _ h   => have := h.isCons; contradiction
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ path₁ ≂ path₂ → prefix? path₁ = prefix? path₂
no goals