intro a
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
⊢ ∀ (a : EdgePath G v w) (q : PathClass G w u) (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) q) r = mul (Quot.mk Reduction a) (mul q r)
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
a : EdgePath G v w
⊢ ∀ (q : PathClass G w u) (r : PathClass G u u'),
    mul (mul (Quot.mk Reduction a) q) r = mul (Quot.mk Reduction a) (mul q r)