Removing symbol countability (issue #12, the sublanguage wrapper)

The step-5/6 theorems assumed [Countable (Σ l, L.Relations l)] for the fair enumeration. This wrapper removes it by the two-sorted symbol-generated sublanguage (symbSublang φ.functionsIn (insert ⟨2, lt⟩ φ.relationsIn) — both sorts countable, proved from the sentence's own symbol supply, with lt inserted so the distinguished relation survives the restriction):

• the well-ordered-chains hypothesis transfers to the sublanguage along reducts;
• the sublanguage endpoint produces the model and rational map;
• expandSymbStructureBase expands the model back to L, preserving the root (realize_restrictSymbols_expandSymbStructureBase) and the relation (dif_pos).

[L.IsRelational] remains — it is consumed by the quotient term model, and its removal is the separate arbitrary-function-language graph translation, not this wrapper.

theorem FirstOrder.Language.exists_model_relPreserving_isRelational {L : Language} [L.IsRelational] (φ : L.Sentenceω) (lt : L.Relations 2) (h : HasWellOrderedChains φ lt) : ∃ (M : Type) (x : L.Structure M) (_ : Nonempty M) (f : ℚ → M), φ.Realize M ∧ RelPreserving lt f

Step-5 endpoint, no symbol countability (relational): the countable-relational-core hypothesis of exists_model_relPreserving_relational removed via the two-sorted sublanguage generated by the sentence's own symbols together with lt.