simp at lm
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
lm : redCons (EdgeBetween.bar (EdgeBetween.bar e)) (redCons (EdgeBetween.bar e) (reverse p)) = reverse p :=
  cancelling_steps_redCons (EdgeBetween.bar e) (reverse p) hyp'
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
lm : redCons e (redCons (EdgeBetween.bar e) (reverse p)) = reverse p
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p