intro c
case mk.mk.mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
b : EdgePath G w u
⊢ ∀ (a_1 : EdgePath G u u'),
    Quot.mk Reduction a * Quot.mk Reduction b * Quot.mk Reduction a_1 =
      Quot.mk Reduction a * (Quot.mk Reduction b * Quot.mk Reduction a_1)
case mk.mk.mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
b : EdgePath G w u
c : EdgePath G u u'
⊢ Quot.mk Reduction a * Quot.mk Reduction b * Quot.mk Reduction c =
    Quot.mk Reduction a * (Quot.mk Reduction b * Quot.mk Reduction c)