rw [bot_adj]
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
x x_1 : α
⊢ Adj G x x_1 ↔ Adj ⊥ x x_1
case Adj.h.h.a
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
h : ∀ (v w : α), v ≠ w → ¬Adj G v w
x x_1 : α
⊢ Adj G x x_1 ↔ False