feat(syntax): regions_introduced_by helper — Phase 3b scaffolding (#225) (#230)

## Summary

Adds \`regions_introduced_by : expr -> list region_name\`, a
\`Fixpoint\` collecting region names introduced by \`ERegion\` subterms.

This is scaffolding infrastructure for Phase D slice 4 Phase 3b
(\`subst_typing_gen_l1_m_tfuneff\`) per ephapax issue #225's recommended
option (a).

## Why now

Phase 3b's main obstacle (per #225 analysis): retyping a TFunEff value
at \`r :: R\` (post T_Region_L1 inside substituee body) requires \`r ∈
R_in_v\`, but \`r\` is fresh and unconstrained relative to \`R_in_v\`.
Option (a) resolves this by adding a syntactic over-approximation
precondition:

\`\`\`coq
(forall r, In r (regions_introduced_by e) -> In r R_in_v)
\`\`\`

The precondition is decomposable through compound rules (each
sub-expression's \`regions_introduced_by\` is a subset of the parent's)
and discharges directly at the \`T_Region_L1\` case (where \`r\` is the
head of \`regions_introduced_by (ERegion r e')\`).

## Why split this scaffold off

The full Phase 3b lemma is ~400 lines mirroring Phase 2 with
\`shift_typing_gen_l1_m\` threading at every binder-descent case (Phase
2's \`ground_nonlinear_value_shift_id_l1\` shortcut doesn't apply to
non-scalar TFunEff lambdas — \`shift c 1 (ELam T0 e0) = ELam T0 (shift
(S c) 1 e0)\`, which changes the body's de Bruijn indices). That scope
exceeds the single-session budget that Phase 1 / Phase 2 / Phase 3a have
been shipping at.

Landing the helper alone keeps a future Phase 3b implementation PR
focused on the lemma body without re-introducing the predicate.

## Verification

\`\`\`
$ cd /tmp/ephapax-phase-3b/formal && just all
coq_makefile -f _CoqProject -o build.mk
make -f build.mk
COQDEP VFILES
COQC Syntax.v
COQC Typing.v
COQC Modality.v
COQC TypingL1.v
COQC Semantics.v
COQC Semantics_L1.v
COQC Counterexample.v
COQC Echo.v
COQC TypingL2.v
COQC L4.v
(exit 0)
\`\`\`

Rocq 9.1.1 / Coq 8.18. Zero new admits, zero new axioms. Helper is
currently unused by any lemma — landing as preparatory infrastructure.

## Owner-directive compliance

- ✅ Does NOT modify \`Semantics.v\`.
- ✅ Does NOT add new admits or axioms.
- ✅ Pure syntactic Fixpoint; no semantic consequences.
- ✅ Lives in \`Syntax.v\` alongside \`is_ground_nonlinear_ty\` and
\`is_tfuneff_ty\` (matching precedent).

## Refs

- ephapax#225 — Phase 3b tracking issue, option (a)
- formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b
- PR #220 — Phase 2 (\`subst_typing_gen_l1_m_ground_nonlinear\`) for
structural template
- PR #228 — Phase 4a (\`preservation_l2_app_eff_beta_linear\`) for Phase
4 use shape

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

formal/Syntax.v

@@ -488,6 +488,34 @@ Definition is_tfuneff_ty (T : ty) : bool :=
   | _ => false
   end.
 
+(** Syntactic over-approximation of region names introduced via
+    [ERegion] subterms of an expression. Used by Phase 3b's TFunEff
+    substitution lemma to discharge the [r ∈ R_in_v] obligation
+    that arises in [T_Region_L1] cases — when the substituee body
+    introduces a region [r], retyping a TFunEff value at the extended
+    [r :: R] requires [r ∈ R_in_v] (the lambda's declared input env).
+
+    Refs [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md] Phase 3b option (a)
+    and ephapax issue #225. *)
+Fixpoint regions_introduced_by (e : expr) : list region_name :=
+  match e with
+  | EUnit | EBool _ | EI32 _ | EVar _
+  | EStringNew _ _ | ELoc _ _ => nil
+  | EStringConcat e1 e2 | ELet e1 e2 | ELetLin e1 e2
+  | EApp e1 e2 | EPair e1 e2 =>
+      regions_introduced_by e1 ++ regions_introduced_by e2
+  | EStringLen e' | EFst e' | ESnd e'
+  | EBorrow e' | EDeref e' | EDrop e' | ECopy e' | EObserve e' =>
+      regions_introduced_by e'
+  | ELam _ e' | EInl _ e' | EInr _ e' | EEcho _ e' =>
+      regions_introduced_by e'
+  | EIf e1 e2 e3 | ECase e1 e2 e3 =>
+      regions_introduced_by e1
+      ++ regions_introduced_by e2
+      ++ regions_introduced_by e3
+  | ERegion r e' => r :: regions_introduced_by e'
+  end.
+
 (** Check if all linear variables in context have been used *)
 Fixpoint ctx_all_linear_used (G : ctx) : Prop :=
   match G with