refactor(core): parameterize mkSeqBoundsPrecond seq input name

Add `seqName : String := "s"` parameter so the helper no longer hardcodes
the input variable name in a string literal three definitions away from
the call sites that depend on it. All four current callers (`Sequence.{select,update,take,drop}`) name their `Sequence a` input `"s"` and use the
default. A future partial Sequence op with a different input name need
only pass it explicitly rather than rely on the hidden literal.

Mismatches between a function's declared inputs and the names used in its
preconditions remain caught at elaboration by `polyUneval`'s `h_precond`
free-vars check; this change only reduces the code-distance between
cause and effect.

Cherry-pick target: PR #1100. The change sits inside #1100's
`mkSeqBoundsPrecond`, so it belongs there. When #1100 lands and this
branch rebases on main, the commit will be deduplicated automatically.

Author: fabiomadge

Strata/Languages/Core/Factory.lean

@@ -521,15 +521,19 @@ private def SeqBoundKind.upperOpExpr : SeqBoundKind → LExpr CoreLParams.mono
   | .Lt => (intLtFunc (T := CoreLParams)).opExpr
   | .Le => (intLeFunc (T := CoreLParams)).opExpr
 
-/-- Precondition `0 <= varName && varName `k.upperOpExpr` Sequence.length(s)`.
-
-    Assumes the enclosing function names its `Sequence a` input `"s"`.
-    Mismatches are caught at elaboration by `polyUneval`'s `h_precond`
-    free-vars check. -/
+/-- Precondition `0 <= varName && varName `k.upperOpExpr` Sequence.length(seqName)`.
+
+    `seqName` defaults to `"s"` since all four current call sites
+    (`Sequence.select`/`update`/`take`/`drop`) name their `Sequence a` input
+    that way. The parameter exists so a future partial Sequence op with a
+    different input name need only pass it explicitly rather than rely on a
+    hidden string literal. Either way, mismatches between the function's
+    declared inputs and the names used here are caught at elaboration by
+    `polyUneval`'s `h_precond` free-vars check. -/
 private def mkSeqBoundsPrecond
-    (varName : String) (k : SeqBoundKind) :
+    (varName : String) (k : SeqBoundKind) (seqName : String := "s") :
     Strata.DL.Util.FuncPrecondition (LExpr CoreLParams.mono) CoreLParams.Metadata :=
-  let sVar  : LExpr CoreLParams.mono := .fvar default "s" (some (seqTy mty[%a]))
+  let sVar  : LExpr CoreLParams.mono := .fvar default seqName (some (seqTy mty[%a]))
   let xVar  : LExpr CoreLParams.mono := .fvar default varName (some mty[int])
   let zero  : LExpr CoreLParams.mono := .intConst default 0
   let lenS  : LExpr CoreLParams.mono := .app default seqLengthFunc.opExpr sVar