rw [h]
case inl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : redCons e p = cons e p
⊢ Even (List.length (toList (redCons e p))) ↔ ¬Even (List.length (toList p))
case inl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : redCons e p = cons e p
⊢ Even (List.length (toList (cons e p))) ↔ ¬Even (List.length (toList p))