simp [prefix?, hi, Option.isSome_iff_exists]
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
child₂ : Class.Child (Class.Child.class child₁)
subpath₂ : Path graph (Class.Child.class child₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi✝ : Option.isSome (prefix? (cons child₂ subpath₂)) = true
subpath : Path graph (Class.Child.class child₁)
hi : prefix? (cons child₂ subpath₂) = some subpath
⊢ Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
child₂ : Class.Child (Class.Child.class child₁)
subpath₂ : Path graph (Class.Child.class child₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi✝ : Option.isSome (prefix? (cons child₂ subpath₂)) = true
subpath : Path graph (Class.Child.class child₁)
hi : prefix? (cons child₂ subpath₂) = some subpath
⊢ ∃ a,
    (do
        let x ← some subpath
        some (cons child₁ x)) =
      some a