induction p with
  | nil =>
    rw [EdgePath.concat]
    simp only [contains_cons, contains_nil, and_congr_right_iff]
    intro he
    have := e.init_eq ▸ H.edges_init e.edge he
    have := e.term_eq ▸ H.edges_terminal e.edge he
    simp_all only
  | cons e p' ih =>
    rw [EdgePath.concat_cons]
    aesop
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ : V
p : EdgePath G a✝¹ a✝
w✝ : V
e : EdgeBetween G a✝ w✝
⊢ contains H (EdgePath.concat p e) ↔ e.edge ∈ H.edges ∧ contains H p
no goals