let ⟨hv, he⟩ := h
V : Type u_1
E : Type u_2
G : Graph V E
H✝ : Subgraph G
u v : V
H H' : Subgraph G
p : EdgePath G u v
hpH : contains H p
h : H ≤ H'
⊢ contains H' p
V : Type u_1
E : Type u_2
G : Graph V E
H✝ : Subgraph G
u v : V
H H' : Subgraph G
p : EdgePath G u v
hpH : contains H p
h : H ≤ H'
hv : H.verts ⊆ H'.verts
he : H.edges ⊆ H'.edges
⊢ contains H' p