rw [← G.ι_bar e]
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ τ G e ∈ H.verts
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ G.ι (G.bar e) ∈ H.verts