haveI : IsEmpty (⊥ : H.Subgraph).verts := by simp
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
⊢ Nonempty (⊥ ≃g ⊥) ∧ ∀ (x : H.Subgraph), ⊥ ≃g x.coe → x = ⊥
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
G✝ G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype β
inst✝ : IsEmpty α
G : SimpleGraph α
H : SimpleGraph β
this : IsEmpty ↑⊥.verts
⊢ Nonempty (⊥ ≃g ⊥) ∧ ∀ (x : H.Subgraph), ⊥ ≃g x.coe → x = ⊥