obtain rfl | hG := eq_or_ne G ⊥
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hGH : ¬G ⊑ H
⊢ G.kill H = H
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hGH : ¬⊥ ⊑ H
⊢ ⊥.kill H = H

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hGH : ¬G ⊑ H
hG : G ≠ ⊥
⊢ G.kill H = H