let h'' := not_iff_self  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:+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)))
h'' : False := not_iff_self h'
⊢ False