simp_all
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₂) = true
w✝¹ : Path graph✝ a✝
hp₁ : prefix? path₁ = some w✝¹
w✝ : Path graph✝ a✝
hp₂ : prefix? path₂ = some w✝
⊢ path₁ ≂ path₂
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ w✝¹ w✝ : Path graph✝ a✝
h : w✝¹ = w✝
hp₁ : prefix? path₁ = some w✝
hp₂ : prefix? path₂ = some w✝
⊢ path₁ ≂ path₂