case mpr =>
  intro h
  induction path
  case nil =>
    have ⟨_, _, _⟩ := isCons_def.mp h
    contradiction
  case cons child₁ subpath₁ hi =>
    cases subpath₁
    case nil => simp [prefix?, Option.isSome]
    case cons child₂ subpath₂ =>
      specialize hi isCons_of_cons
      have ⟨subpath, hi⟩ := Option.isSome_iff_exists.mp hi
      simp [prefix?, hi, Option.isSome_iff_exists]
      exists .cons child₁ subpath
graph : Graph
start : Class graph
path : Path graph start
⊢ isCons path = true → Option.isSome (prefix? path) = true
no goals