case inl hp =>
  have ⟨_, hp₁⟩ := Option.isSome_iff_exists.mp hp
  rw [h] at hp
  have ⟨_, hp₂⟩ := Option.isSome_iff_exists.mp hp
  simp_all
  exact Sibling.cons hp₁ hp₂
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂
no goals