proof(L1.C): subst_preserves_typing_l1 Qed (with strengthened statement) (#160)

## Summary

Third of three swarm-dispatched helper lemmas for \`preservation_l1\`
(task #23 / L1.C).

Substitution lemma for \`has_type_l1\`. Closes β-reduction cases of
preservation (S_Let_Val, S_LetLin_Val, S_App_Fun, S_Case_Inl,
S_Case_Inr).

## Strengthened statement

The original lemma in PR #157 was **demonstrably unsound**
(counterexample with R1=[r], R2=[], v=ELoc l r). The new statement types
v at R2; G2 (body's input), which β-reduction sites satisfy after
value_R_G_preserving_l1 (L1.A).

## What's added

571 LOC of new infrastructure (all Qed):

- \`typing_preserves_length_l1\`, \`typing_preserves_bindings_l1\`
- \`unrestricted_flag_unchanged_l1\`,
\`flag_false_to_true_implies_linear_l1\`
- \`output_shape_at_l1\`, \`value_R_G_invariant_l1\`
- \`canonical_string_l1\`, \`linear_value_is_loc_l1\`, \`loc_typing_l1\`
- \`shift_typing_gen_l1\`, \`subst_typing_gen_l1\`

These mirror the legacy Semantics.v support lemmas for substitution.

## Residual: one sub-Axiom

\`loc_retype_at_R_l1\` — an ELoc l r retypes at any R' containing r.
Captures L1 region-extension; should follow from a structural
region-liveness invariant. Sequenced as task #27.

## Net admit/axiom count

Was 3 Admitted (after L1.A+L1.B) + 0 Axiom. Now 2 Admitted
(\`region_shrink_preserves_typing_l1_gen\`, \`preservation_l1\`) + 1
Axiom (\`loc_retype_at_R_l1\`). subst_preserves_typing_l1 converted from
Admitted to Qed.

## Test plan

- [x] \`coqc 8.18.0\` builds Semantics_L1.vo cleanly
- [x] Target lemma Qed
- [x] L1.A's value proof + L1.B's region_shrink still Qed (no
regression)
- [ ] CI green

Base: \`proof/l1-region-threading-design\` (rebased onto L1.A + L1.B
merge commits; docstring conflict resolved with combined honest status).

Refs ephapax#157, ephapax#158, ephapax#159, tasks #23 / #27.

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

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

Author: hyperpolymath