proof(coq): close 10 of 22 preservation goals via per-case manual proofs (#116)

## Summary

**Preservation existential count: 22 → 12** (10 goals closed).

Builds on the region-invariance lemma `step_R_eq_or_touches_region` (PR
#114) by adding per-step-constructor manual proof scripts inside
`Theorem preservation`.

## Closed (10 step constructors)

| Constructor | Closure technique |
|---|---|
| `S_Let_Val`, `S_LetLin_Val` | β-reduction via `subst_preserves_typing`
+ `value_context_unchanged` |
| `S_App_Fun` | Inversion of `ELam` typing + value-context invariance on
arg |
| `S_If_True`, `S_If_False` | Branch typing under `VBool`'s
unchanged-ctx via `value_context_unchanged` |
| `S_Fst`, `S_Snd` | `EPair` inversion → child typing match |
| `S_Case_Inl`, `S_Case_Inr` | `EInl` / `EInr` typing inversion + body
substitution |
| `S_Copy` | `T_Pair` on non-linear value with equal pre/post context |

## Open (12 remaining)

**11 congruence cases** (`S_StringConcat_Step1/2`, `S_StringLen_Step`,
`S_Let_Step`, `S_LetLin_Step`, `S_App_Step1/2`, `S_If_Step`,
`S_Pair_Step1/2`, `S_Case_Step`).

Root cause: the **linearity-context drift** I diagnosed earlier — even
after `step_R_eq_or_touches_region` puts us in the `R = R'` branch, the
IH's output context (a Skolem variable from `edestruct`) doesn't unify
with the sibling premise's pre-context. So `eapply T_Foo; [exact Hout |
exact Hsibling]` fails on the middle-context unification.

The tactic-block scaffolding for these 11 cases is in place (poses
`step_R_eq_or_touches_region`, dispatches the LEFT branch, specialises
`IHHstep`), with the final reconstruction silently failing — they fall
through to `Admitted`. The right next step is **lemma B**: a "step
preserves output linearity context" or context-transfer re-typing via
the existing `typing_ctx_transfer`/`type_determinacy` machinery.

**1 region case** (`S_Region_Step` + `T_Region_Active`): the documented
language-design blocker — region-env weakening for non-values. Tracked
in `formal/PRESERVATION-HANDOFF.md`.

## Verification

```
$ coqc -Q . Ephapax Semantics.v
(builds clean; Admitted preservation now at 12 existentials)
```

## Refs

- `standards#124` (proof-debt audit epic)
- `ephapax#102` (910 → 29 via remember-cfg)
- `ephapax#106` (29 → 22 via universal-IH revert)
- `ephapax#114` (region-invariance lemma — used here)

## Cumulative

| State | Open goals |
|---|---:|
| Pre-#102 | 910 |
| Post-#102 | 29 |
| Post-#106 | 22 |
| **Post this PR** | **12** |

98.7% reduction across the day from start of campaign.

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

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

Author: hyperpolymath