cases lem
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₁ := terminal₀_eq_of_r H contra
⊢ False
case a.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ : V
p : EdgePath G x₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra
⊢ False