FOL: bundle the structure (D, I, F) into a Lean structure #35

Since #34, the prose of CSwL/Logic/FOL.lean presents a structure as 𝒜 = (D, I), or 𝒜 = (D, I, F) when there are function symbols. The code does not match: the domain, the interpretations and the assignment are passed as separate arguments (Interp D/Denot D, FInterp D, Assign D), and the prose has to tell the reader which arguments together form "the structure".

Proposal: introduce a Lean structure that bundles the domain's interpretations, e.g.

structure Structure (D : Type) where
  rel  : String → List D → Prop   -- or Bool, for `eval`
  func : String → List D → D

and state eval, denote, Valid, Satisfiable and Implies in terms of it.

To decide:

• Whether to align with Mathlib's FirstOrder.Language.Structure (typed signature, arities in the type), or keep the string-named, untyped symbols the chapter uses now. Reusing Mathlib is a project goal, but its encoding may cost more Lean than the chapter has introduced so far (see the ledger in STYLE-CODE.md).
• How the Bool (eval, finite domains) and Prop (denote) sides share the bundle.
• The effect on the exercises (ex-fol-weak-strong, ex-fol-valid, ex-fol-implies-from-list, ex-fol-entails) and on the English chapter (Revise ModelChecking.lean #15, feat(ModelChecking): write the chapter from CSwFP/6.1, 4.2, 6.2 and 6.3–6.4 #29), which will build models for the translated fragment.

Related: the issue on Valid/ValidT.