∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] [inst_1 : SizeOf M] (carrier : Set M)
  (fun_mem : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier),
  sizeOf { carrier := carrier, fun_mem := fun_mem } = 1