Theorem: Graph.redCons_cons_edge_eq (GroupComp/Graph/ReducedPaths.lean)

State before:
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
e' : EdgeBetween G v u
p : EdgePath G u w
h : e' = EdgeBetween.bar e
⊢ redCons e (cons e' p) = p
Tactic:
simp [redCons, h]
State after:
no goals