intro h
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂✝ : EdgePath G v₂✝ w₂✝
v₁' w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂ : EdgePath G w✝ w₂
⊢ toList (nil v₁') = toList (cons e₂ p₂) → v₁' = v₂ → v₁' = w₂
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂✝ : EdgePath G v₂✝ w₂✝
v₁' w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂ : EdgePath G w✝ w₂
h : toList (nil v₁') = toList (cons e₂ p₂)
⊢ v₁' = v₂ → v₁' = w₂