∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (s : Set M),
  s ∈ (FirstOrder.Language.Substructure.closure L).closed ↔
    ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f s