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 start✝ : Class graph
child₁ : Class.Child start✝
child₂ : Class.Child (Class.Child.class child₁)
subpath₂ : Path graph (Class.Child.class child₂)
hi : isCons (cons child₂ subpath₂) = true → Option.isSome (prefix? (cons child₂ subpath₂)) = true
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
⊢ Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
no goals