induction p with
  | nil => simp only  [contains_nil, EdgePath.reverse_nil, imp_self]
  | cons e p' ih =>
    rw [EdgePath.reverse_cons]
    simp only [contains_cons, contains_concat, EdgeBetween.bar_eq_bar, and_imp]
    intro he hp'H
    exact ⟨H.edges_bar _ he, ih hp'H⟩
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v : V
p : EdgePath G u v
⊢ contains H p → contains H (EdgePath.reverse p)
no goals