∀ (L : FirstOrder.Language) (n : ℕ),
  FirstOrder.Language.Sentence.cardGe L n =
    (List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤
        (List.map
          (fun ij =>
            (((FirstOrder.Language.var ∘ Sum.inr) ij.1).bdEqual ((FirstOrder.Language.var ∘ Sum.inr) ij.2)).not)
          (List.filter (fun ij => decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)))).exs