rw [this] at h'
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
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ ¬Even (List.length (EdgePath.toList e.p)) :=
  concat_parity e.p e.nxt
⊢ False
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
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ ¬Even (List.length (EdgePath.toList (e.p:+e.nxt)))
⊢ False