rfl
case Adj.h.h.a
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
inst✝ : DecidableRel H.Adj
u v : α
⊢ Adj G u v \ Adj H u v ↔ Adj G u v ∧ ¬Adj H u v
no goals