rw [← contra]
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
⊢ List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (bar G x₀ e).p)
no goals