∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} [inst : DecidableEq α],
  Maximal (fun H => H.CliqueFree (n + 1)) G →
    ∀ {x y : α}, x ≠ y → ¬G.Adj x y → ∃ s, x ∉ s ∧ y ∉ s ∧ G.IsNClique n (insert x s) ∧ G.IsNClique n (insert y s)