case inr hp =>
  have hc₁ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp; simp at hc₁
  rw [h] at hp
  have hc₂ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp; simp at hc₂
  simp [hc₁, hc₂, Sibling.nil]
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