wip(L1): Phase 3b Stage 1b — body-transfer + closed-value G-poly helpers

Path-(i) machinery for the elegance-first Stage 1b. Closed TFunEff
values are typed at ANY G — for closed values, G is genuinely
irrelevant. The substitution lemma's compound-rule cases (next
commit) consume this fact to discharge the G-mismatch gap that
blocks `tfuneff_lambda_retype_l1_m` (G-preserving) from playing
the same role Phase 2's `ground_nonlinear_retype_l1_m` plays for
ground non-linear values.

Ships:

(1) `ctx_mark_used_app_lt` in Syntax.v — [ctx_mark_used] commutes
    with context append when the marked position lies within the
    head. Required by body-transfer's T_Var_Lin_L1 case (the only
    typing rule that changes G's flags).

(2) `closed_below_k_typing_outer_tail_irrelevant_l1_m` in
    Semantics_L1.v — the body-transfer core. Structural induction
    on the typing derivation across 28+ rule cases. Statement:

      forall m R G e T R' G_out,
        has_type_l1 m R G e T R' G_out ->
        forall k G_head G_tail,
          G = G_head ++ G_tail ->
          length G_head = k ->
          expr_closed_below k e = true ->
          exists G_head_out,
            G_out = G_head_out ++ G_tail /\
            length G_head_out = k /\
            forall G_tail_new,
              has_type_l1 m R (G_head ++ G_tail_new) e T R'
                (G_head_out ++ G_tail_new).

    "Closed below k terms' typing depends only on G's first k
    positions; the outer tail is structurally irrelevant." Each
    typing-rule case threads (k, G_head, G_tail) through its
    sub-derivations and reconstructs the rule at the alternate
    tail. Binder rules (T_Let / T_LetLin / T_Lam_* / T_Case_*)
    apply IH at k+1 with the binder type cons'd onto G_head;
    Case rules cross-check branch agreement via `app_inv_tail`.

(3) `closed_value_typing_G_poly_l1_m` in Semantics_L1.v — the
    consumer-facing helper. Statement (any-G' form per
    elegance-first decision: state what's actually true, not what
    fell out of the proof induction):

      is_value v -> expr_closed_below 0 v = true ->
      has_type_l1 m R G  v (TFunEff T1 T2 R_in R_out) R G ->
      has_type_l1 m R G' v (TFunEff T1 T2 R_in R_out) R G'.

    Proof: invert is_value + has_type_l1 to T_Lam_L1_*_Eff cases;
    apply body-transfer at k=1, G_head=[(T1,false)], G_tail=G.

(4) `closed_value_shift_id_l1_m` in Semantics_L1.v — companion:
    closed values' [shift 0 d] is identity. Specialises
    [Syntax.closed_below_shift_id] for the subst lemma's binder
    cases where [shift 0 1 v] must reduce to [v] for the typing
    reconstruction to fire.

Owner-directive compliance (CLAUDE.md 2026-05-27):
- ✅ No touch to formal/Semantics.v / Typing.v / Counterexample.v.
- ✅ No closure of residual Semantics_L1.v admits attempted.
- ✅ Anti-pattern detector clean (canonical CS infrastructure;
  no sibling-region-disjointness, no region-weakening predicates
  on syntactic shape, no admit-shuffling, no legacy-preservation
  closure attempt).
- ✅ Strictly NEW infrastructure orthogonal to legacy.

Build oracle (coqc 8.18.0): clean across all 12 .v files post-edit.

Next commit on this branch: `subst_typing_gen_l1_m_tfuneff` Qed
(~300 lines mirroring Phase 2 with the closed-value G-poly helper
replacing `ground_nonlinear_retype_l1_m` where G-poly retype is
needed). Then `preservation_l2_app_eff_beta_tfuneff_l1` + L2
wrapper in TypingL2.v.

Refs:
- ephapax issue #249 (Stage 1b tracking, this commit partial)
- ephapax PR #252 (Stage 1a prerequisite — tfuneff_lambda_free
  + Counterexample_L2_nested)
- ephapax issue #239 (parent Stage 1)
- formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b Stage 1b

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

Author: hyperpolymath