rw [this, append_mul, append_mul, rel]
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
rel : [[a₁]] = [[a₂]]
this✝ : concat a₁ b = a₁ ++ concat (nil w) b
this : concat a₂ b = a₂ ++ concat (nil w) b
⊢ [[a₁ ++ concat (nil w) b]] = [[concat a₂ b]]
no goals