have := e.init_eq ▸ H.edges_init e.edge he
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
he : e.edge ∈ H.edges
⊢ w✝ ∈ H.verts ↔ v✝ ∈ H.verts
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
he : e.edge ∈ H.edges
this : v✝ ∈ H.verts
⊢ w✝ ∈ H.verts ↔ v✝ ∈ H.verts