simp only [contains_cons, contains_concat, EdgeBetween.bar_eq_bar, and_imp]
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
⊢ contains H (EdgePath.cons e p') → contains H (EdgePath.concat (EdgePath.reverse p') (EdgeBetween.bar e))
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
⊢ e.edge ∈ H.edges → contains H p' → G.bar e.edge ∈ H.edges ∧ contains H (EdgePath.reverse p')