exact fun hab ↦ e.symm.map_rel_iff.2 hab.coe
case h.e'_2.h.e'_2.refine'_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
H' : H.Subgraph
e : ⊥ ≃g H'.coe
a b : β
⊢ ¬H'.Adj a b
no goals