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

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v v' w : V
e : EdgeBetween G u v
e' : EdgeBetween G v v'
p : EdgePath G v' w
h : v' ≠ u
⊢ redCons e (cons e' p) = cons e (cons e' p)
Tactic:
simp [redCons, h]
State after:
no goals