apply H.edges_bar
case a
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ G.bar e ∈ H.edges
case a.a
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ e ∈ H.edges