case mpr.cons child subpath =>
  have hs := prefix?_isSome_iff_isCons.mpr (@isCons_of_cons _ _ child subpath)
  have ⟨_, hs⟩ := Option.isSome_iff_exists.mp hs
  simp [hs, prefix?] at h ⊢
  injection h with h
  injection h
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
⊢ prefix? (cons child subpath) = some path₂
no goals