case mp =>
  intro h
  induction path
  case nil => simp [prefix?] at h
  case cons child₁ subpath₁ hi =>
    cases subpath₁
    case nil => rfl
    case cons child₂ subpath₂ => simp [isCons]
graph : Graph
start : Class graph
path : Path graph start
⊢ Option.isSome (prefix? path) = true → isCons path = true
no goals