simp only [contains_cons, contains_nil, and_congr_right_iff]
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
⊢ contains H (EdgePath.cons e (EdgePath.nil w✝)) ↔ e.edge ∈ H.edges ∧ contains H (EdgePath.nil v✝)
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝ v✝ : V
e : EdgeBetween G v✝ w✝
⊢ e.edge ∈ H.edges → (w✝ ∈ H.verts ↔ v✝ ∈ H.verts)