apply hv
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H✝ : Subgraph G
u v : V
H H' : Subgraph G
h : H ≤ H'
hv : H.verts ⊆ H'.verts
he : H.edges ⊆ H'.edges
v✝ : V
hpH : contains H (EdgePath.nil v✝)
⊢ contains H' (EdgePath.nil v✝)
case nil.a
V : Type u_1
E : Type u_2
G : Graph V E
H✝ : Subgraph G
u v : V
H H' : Subgraph G
h : H ≤ H'
hv : H.verts ⊆ H'.verts
he : H.edges ⊆ H'.edges
v✝ : V
hpH : contains H (EdgePath.nil v✝)
⊢ v✝ ∈ H.verts