convert
  card_singleton
    ({  verts := Set.univ
        Adj := ⊥
        adj_sub := False.elim
        edge_vert := False.elim } : H.Subgraph)
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H✝ : SimpleGraph β
I : SimpleGraph γ
inst✝ : Fintype β
H : SimpleGraph β
⊢ (filter (fun H' => Nonempty (⊥ ≃g H'.coe)) univ).card = 1
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 β
H : SimpleGraph β
⊢ filter (fun H' => Nonempty (⊥ ≃g H'.coe)) univ =
    {{ verts := Set.univ, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }}