induction rel
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 : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
rel : Reduction b₁ b₂
⊢ [[a ++ b₁]] = [[a ++ b₂]]
case step
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 : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ (p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝))]] = [[a ++ (p₁✝ ++ p₂✝)]]