rw [EdgePath.concat_cons]
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝¹ v✝ w✝ u✝ : V
e✝ : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : ∀ {e : EdgeBetween G u✝ w✝¹}, contains H (EdgePath.concat p' e) ↔ e.edge ∈ H.edges ∧ contains H p'
e : EdgeBetween G u✝ w✝¹
⊢ contains H (EdgePath.concat (EdgePath.cons e✝ p') e) ↔ e.edge ∈ H.edges ∧ contains H (EdgePath.cons e✝ p')
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
a✝¹ a✝ w✝¹ v✝ w✝ u✝ : V
e✝ : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : ∀ {e : EdgeBetween G u✝ w✝¹}, contains H (EdgePath.concat p' e) ↔ e.edge ∈ H.edges ∧ contains H p'
e : EdgeBetween G u✝ w✝¹
⊢ contains H (EdgePath.cons e✝ (EdgePath.concat p' e)) ↔ e.edge ∈ H.edges ∧ contains H (EdgePath.cons e✝ p')