simp only  [contains_nil, EdgePath.reverse_nil, imp_self]
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ : V
⊢ contains H (EdgePath.nil v✝) → contains H (EdgePath.reverse (EdgePath.nil v✝))
no goals