Define typing relation for commands and prove soundness of typechecker

[joscoh]

Gives a type specification for commands (CmdHasType'), generalized over the LExpr typing relation, and instantiates it with LExpr.hasType (CmdHasType) and LExpr.hasTypeA (CmdHasTypeA). Proves that:

1. If the command typechecker Cmd.typeCheck succeeds, then the original command was well-typed according to CmdHasType (theorem Cmd.typeCheck_sound).
2. If Cmd.typeCheck succeeds, then the output command is well-annotated according to CmdHasTypeA (theorem Cmd.typeCheck_annotated_sound).

Core command typing (new files under Strata/Languages/Core/)

• CmdTypeSpec.lean — the inductive CmdHasType', parameterized over an
  ExprTypingSpec typeclass with two instances: CmdHasType (polymorphic
  HasType, over LTy) and CmdHasTypeA (annotated HasTypeA, over
  LMonoTy).
• CmdTypeSpecProps.lean — the two top-level soundness theorems,
  Cmd.typeCheck_sound and Cmd.typeCheck_annotated_sound, showing
  Cmd.typeCheck produces commands satisfying the spec.
• CmdTypeProps.lean — supporting lemmas about preprocess / inferType
  / unifyTypes and context updates that feed the soundness proofs.
• CmdType.inferType — no longer auto-registers undeclared free variables
  via addInOldestContext. Expressions in init/set/assert/assume/cover
  that reference variables not already in scope are now rejected by freeVarCheck.
  Previously, undeclared variables were silently added, which is not longer needed
  with nondeterministic init.

Rigid type variables (fixes #1345)

• CmdType.checkAnnotCompat — new checker pass that rejects any unification
  result refining a rigid (skolemized) type variable.
• ProcedureType.lean — setupInputEnv now generates fresh rigid vars for
  type parameters and records them in C.rigidTypeVars; body typechecking
  enforces identity on these vars via checkAnnotCompat.
• CmdTypeSpec.lean — the init_det/init_nondet constructors use
  RigidAnnotCompat (AnnotCompat restricted to be identity on rigid vars).
• CmdTypeSpecProps.lean — Cmd.typeCheck_preserves_rigid_inv proves the
  invariant is preserved; typeCheck_sound uses it.
• RigidTypeVarsTests.lean — test cases for polymorphic procedures with
  rigid type parameters, including expected-failure cases.

Lambda layer

• LExprResolveProps.lean (renamed from LExprResolveAnnotated.lean) adds theorem resolve_eqModuloAnnotations (resolution preserves
  expression structure, changing only metadata and annotations).
• LExprTypeSpec.lean — adds freshness / TEnvWF / well-scoped supporting
  lemmas used by the resolve and command proofs. The HasType relation itself
  is unchanged.
• LExprTypeEnv.lean — adds TContext.subst and TEnv lemmas
  (substitution lookup, addInNewestContext, free-variable scoping) used by the
  command proofs.
• Smaller supporting changes in LExprWF.lean and LTyUnify.lean.

Tooling

• Strata/Util/Tactics.lean — now contains the elim_err / elim_errs tactics for
  discharging error branches when unfolding Except-valued checker code, used
  throughout the soundness proofs.