intro h
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ (¬∃ v w, v ≠ w ∧ Adj G v w) → ¬G ≠ ⊥
α : 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
⊢ ¬G ≠ ⊥