proof(L1.A): value_R_G_preserving_l1 Qed (#158)

## Summary

First of three swarm-dispatched helper lemmas for \`preservation_l1\`
(task #21 / L1.A).

\`value_R_G_preserving_l1\` — every value form under the L1 judgment
preserves both R and G (R_out = R_in, G_out = G_in).

**32 LOC of proof body**, no other admits touched.

## Proof structure

- Induction on \`is_value\` with \`revert R G T R' G'\` before induction
for fully-general IHs.
- Atomic values (VUnit, VBool, VI32, VLam, VLoc): single \`inversion\` +
\`split; reflexivity\`.
- Compound values (VPair, VInl, VInr): match goal picks typing premise,
apply IH on sub-value.
- VBorrow: T_Borrow_L1 sub-case (inner = EVar) discharged by
\`inversion\` on the value hypothesis (values can't be EVars).

## What this unblocks

The simple congruence (S_X_Step) cases of \`preservation_l1\` in
Semantics_L1.v can now be inlined — they need this helper to thread R/G
across the value-stepping sub-expression.

## Test plan

- [x] \`coqc 8.18.0\` builds \`Semantics_L1.vo\` cleanly (0 admits on
this lemma)
- [x] Other 3 admits (region_shrink_preserves_typing_l1,
subst_preserves_typing_l1, preservation_l1) UNTOUCHED — separate swarm
agents handle those (L1.B, L1.C; L1.D depends on all three)
- [ ] CI green

Base: \`proof/l1-region-threading-design\` (PR #153, currently bundling
all L1 work). Will rebase onto main once #153 lands.

Refs ephapax#157 (Semantics_L1.v skeleton), task #21.

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

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

Author: hyperpolymath

formal/Semantics_L1.v

@@ -93,7 +93,44 @@ Lemma value_R_G_preserving_l1 :
     is_value v ->
     has_type_l1 R G v T R' G' ->
     R' = R /\ G' = G.
-Admitted.
+Proof.
+  intros R G v T R' G' Hv. revert R G T R' G'.
+  induction Hv; intros R0 G0 T0 R0' G0' Ht.
+  - (* VUnit *) inversion Ht; subst; split; reflexivity.
+  - (* VBool *) inversion Ht; subst; split; reflexivity.
+  - (* VI32 *) inversion Ht; subst; split; reflexivity.
+  - (* VLam *) inversion Ht; subst; split; reflexivity.
+  - (* VPair v1 v2 *)
+    inversion Ht; subst.
+    match goal with
+    | [ H1 : has_type_l1 _ _ v1 _ _ _,
+        H2 : has_type_l1 _ _ v2 _ _ _ |- _ ] =>
+        specialize (IHHv1 _ _ _ _ _ H1) as [HR1 HG1]; subst;
+        specialize (IHHv2 _ _ _ _ _ H2) as [HR2 HG2]; subst
+    end.
+    split; reflexivity.
+  - (* VInl T v *)
+    inversion Ht; subst.
+    match goal with
+    | [ H : has_type_l1 _ _ v _ _ _ |- _ ] =>
+        specialize (IHHv _ _ _ _ _ H) as [HR HG]; subst
+    end.
+    split; reflexivity.
+  - (* VInr T v *)
+    inversion Ht; subst.
+    match goal with
+    | [ H : has_type_l1 _ _ v _ _ _ |- _ ] =>
+        specialize (IHHv _ _ _ _ _ H) as [HR HG]; subst
+    end.
+    split; reflexivity.
+  - (* VLoc *) inversion Ht; subst; split; reflexivity.
+  - (* VBorrow v *)
+    inversion Ht; subst.
+    + (* T_Borrow_L1: EBorrow (EVar i) — impossible since v is a value, not EVar *)
+      inversion Hv.
+    + (* T_Borrow_Val_L1 *)
+      split; reflexivity.
+Qed.
 
 (** ** Helper: region-environment shrinkage for value typings.