intro ⟨τ₀, τ₁, e, p, pf⟩
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (a : Edge G x₀), ⟦a⟧ ≠ bar H ⟦a⟧
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
⊢ ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧ ≠
    bar H ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧