Theorem: Graph.Subgraph.contains_append (GroupComp/Subgraph.lean)

State before:
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v w : V
p : EdgePath G u v
p' : EdgePath G v w
⊢ contains H (p ++ p') ↔ contains H p ∧ contains H p'
Tactic:
induction p <;> aesop
State after:
no goals