cases prepend_cases e p with
| inl h =>
  rw [h]
  simp only [cons_toList, List.length_cons]
  apply Nat.even_add_one
| inr h =>
  let ⟨t, h₁, h₂⟩ := h
  rw [h₂, h₁]
  simp  [cons_toList, List.length_cons, Nat.even_add_one]
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
⊢ Even (List.length (toList (redCons e p))) ↔ ¬Even (List.length (toList p))
no goals