simp at hpH ⊢
case cons
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✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H' p'
hpH : contains H (EdgePath.cons e p')
⊢ contains H' (EdgePath.cons e p')
case cons
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✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H' p'
hpH : e.edge ∈ H.edges ∧ contains H p'
⊢ e.edge ∈ H'.edges ∧ contains H' p'