rw [kill_of_ne_bot hG, deleteEdges, isContained_iff_exists_subgraph]
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
⊢ ¬G ⊑ G.kill H
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
⊢ ¬∃ H', Nonempty (G ≃g H'.coe)