proof(L3): preservation_l3 capstone — slice 4 (closes L3 wiring) (#196)

## Summary

**L3 wiring slice 4 — capstone.** Per-layer preservation theorem for the
two L3-specific echo-emitting step rules paired with their matching L3
typing rules. Closes the L3 wiring task in `PROOF-NEEDS.md §2`.

## What's new

Three new Qed in `formal/Semantics_L1.v`:

| Lemma | What it proves |
|---|---|
| `preservation_l3_region_active_echo` | `(T_Region_Active_L1_Echo,
S_Region_Exit_Echo)` pair preserves typing at `TEcho T` |
| `preservation_l3_drop_echo` | `(T_Drop_L1_Echo, S_Drop_Echo)` pair
preserves typing at `TEcho T` |
| `preservation_l3` (umbrella) | Conjunction of the two — Qed by `split;
exact …` |

Per-case alignment is **forced by `T_Echo_L1`'s witness-type premise**.
The step rules are universally quantified over `T` (non-deterministic at
the relation level); the typing derivation pins which `T` is in play.
Non-deterministic crossover cases (e.g. legacy `T_Region_Active_L1` + L3
`S_Region_Exit_Echo`) are non-preserving by design — not covered by this
theorem and not well-typed at the umbrella's `TEcho T` output.

## Seam audit (every admit/axiom classified)

The user asked to "make sure that all the seams and gaps are checked and
secure." Two outcomes:

### 1. One avoidable parallel-rule admit closed

`region_shrink_preserves_typing_l1_gen_m`'s `T_Region_L1_Echo` case
admit (was a mirror of a **fully-closed** original) is now Qed-style —
count-monotonicity for the shadowed sub-case, `remove_first` commutation
for the descend sub-case. Same treatment for the descend sub-case of
`T_Region_Active_L1_Echo`. **Net debt: -1 internal admit.**

### 2. Every remaining admit classified in PROOF-NEEDS.md §4

After this PR, the complete admit/axiom inventory of `formal/*.v`:

| Location | Class |
|---|---|
| `Semantics_L1.v:553` (`admit.`) | Pre-existing L1 structural
(T_Region_Active_L1 shadowed) |
| `Semantics_L1.v:621` (`admit.`) | True parallel mirror of `:553` |
| `Semantics_L1.v:653` (`Admitted.`) | Outer marker over `:553` + `:621`
|
| `Semantics_L1.v:1256` (`admit.`) | Pre-existing L1 structural
(T_Region_Active_L1 `r = rv`) |
| `Semantics_L1.v:1276` (`admit.`) | True parallel mirror of `:1256` |
| `Semantics_L1.v:1290` (`Admitted.`) | Outer marker over `:1256` +
`:1276` |
| `Semantics_L1.v:1694` (`admit.`) | Pre-existing — `preservation_l1`
lambda-rigidity gap |
| `Semantics_L1.v:1695` (`Admitted.`) | Outer marker over `:1694` |
| `Semantics.v:9257` (`Admitted.`) | 🛑 Sacrosanct (provably false per
`Counterexample.v`) |

**Zero `Axiom` declarations**. `TypingL1.v` / `Modality.v` / `Echo.v` /
`Counterexample.v` / `TypingL2.v` are all admit-free.

## Per CLAUDE.md owner directive 2026-05-27

- ✅ Zero new `Admitted.` or `Axiom.` declarations
- ✅ No legacy `Semantics.v` patching
- ✅ No cross-layer reasoning to close L1 admits
- ✅ Re-uses pre-existing infrastructure only (`value_R_G_preserving_l1`
Qed + `region_shrink_preserves_typing_l1_gen_m` conditional)
- ✅ Cross-layer dependency on L1 structural admit annotated per
`PRESERVATION-DESIGN.md §5.1`

## Build oracle

`coqc 8.18.0` clean rebuild of all 9 `.v` files in dependency order:
PASS.

## Test plan

- [x] Slice 4 lemmas compile with zero warnings
- [x] All 9 `formal/*.v` files compile (`coqc -R . Ephapax`)
- [x] Zero new `admit.` or `Admitted.` introduced (verified via grep)
- [x] One avoidable parallel-rule admit closed (line 574 was; gone now)
- [x] Commit GPG-signed (`G` per `git log --format=%G?`)
- [ ] CI green
- [ ] Owner review

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

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

Author: hyperpolymath

PROOF-NEEDS.md

@@ -56,7 +56,7 @@ For the architectural background see
 | L1 judgment indexed by modality `m : Modality` | `formal/TypingL1.v` | landed via PRs #176 + #177 |
 | L2 modality core (`Modality.v`, `linear_to_affine`) | `formal/Modality.v` | 1 Qed, zero axioms |
 | L3 calculus (echo / residue fiber + degrade + no-section proof) | `formal/Echo.v` | 12 Qed, 0 admits |
-| Linear-mode forward progress lemmas | `formal/Semantics_L1.v` | 23 Qed; 3 residual admits (L2-β follow-up) |
+| Linear-mode forward progress lemmas | `formal/Semantics_L1.v` | 26 Qed (incl. 3 new from L3 slice 4: `preservation_l3_region_active_echo` / `preservation_l3_drop_echo` / `preservation_l3` umbrella); 3 outer `Admitted.` markers cover 5 internal `admit.` cases — all pre-existing L1 structural debt OR true parallel mirrors |
 | Counterexample regression witness | `formal/Counterexample.v` | 5 Qed (`bad_input_untypable_l1` proved under both modes) |
 | Operational checker (Rust, ephapax-linear sublanguage) | `ephapax-linear/src/linear.rs` | working — discharges resource-exact obligation |
 
@@ -106,10 +106,10 @@ enters the typing rules" and (for the diagram) in §6 (to be added).
 | ✅ Extend AST with [TEcho : ty -> ty] and [EEcho : ty -> expr -> expr] | Type former + runtime value form for L3 echoes | done 2026-05-27 (L3 wiring slice 1 — Syntax.v + free_regions + value/shift/subst cases) |
 | ✅ Add `T_Observe_L1` typing rule + `EObserve` expr form | Consumes a `TEcho T` echo, returns `TBase TUnit` | done 2026-05-27 (L3 wiring slice 2 — modality-polymorphic single rule; mandatoriness via `is_linear_ty TEcho`/implicit-drop discipline is a follow-up) |
 | ✅ Add `T_Echo_L1` typing rule | Types runtime [EEcho T v] residue values at `TEcho T` | done 2026-05-27 (L3 wiring slice 3a — typing-side counterpart of forthcoming `S_Region_Exit_Echo` / `S_Drop_Echo` step rules; mode-polymorphic) |
-| ✅ Add parallel typing rules `T_Region_L1_Echo` / `T_Region_Active_L1_Echo` / `T_Drop_L1_Echo` | Output `TEcho T` instead of `T` / `TBase TUnit`. Programs choose at typing time which path | done 2026-05-27 (L3 wiring slice 3b — owner-approved parallel-rule strategy). +3 internal admits in [region_shrink_preserves_typing_l1_gen_m] + [region_liveness_at_split_l1_gen] are parallel-rule MIRRORS of pre-existing structural admits, NOT new structural debt |
+| ✅ Add parallel typing rules `T_Region_L1_Echo` / `T_Region_Active_L1_Echo` / `T_Drop_L1_Echo` | Output `TEcho T` instead of `T` / `TBase TUnit`. Programs choose at typing time which path | done 2026-05-27 (L3 wiring slice 3b — owner-approved parallel-rule strategy). Initial +3 internal admits in [region_shrink_preserves_typing_l1_gen_m] + [region_liveness_at_split_l1_gen] were parallel-rule MIRRORS of pre-existing structural admits; the avoidable T_Region_L1_Echo mirror was CLOSED in slice 4 — only the two true T_Region_Active_*_L1_Echo shadowed-case mirrors remain, both blocked by the same pre-existing list-vs-multiset structural debt as the originals |
 | ✅ Add collapse-function emission to step rules at irreversible boundaries | `S_Region_Exit_Echo` emits `EEcho T v` paralleling `S_Region_Exit` (untouched); `S_Drop_Echo` emits `EEcho T (ELoc l r)` paralleling `S_Drop` | done 2026-05-27 (L3 wiring slice 3c — owner-approved parallel-rule strategy in Semantics.v; updated `step_from_eregion` to 4-disjunct classification + `step_R_change_shape` + `no_leaks_gen` cascade); rules quantified over witness type T |
 | ~~Thread `G` (echo context) alongside `R` (region context) through compound rules~~ | ~~New context parameter on every L1 compound rule~~ | **OBSOLETE 2026-05-27**: under the owner-approved parallel-rules design (slices 3a–3c), echoes are values of type `TEcho T` that flow through the existing `ctx` G. No separate echo-context parameter is needed. |
-| State and prove `preservation_l3` | Per-layer preservation theorem against the L3 invariants for the new echo-emitting step rules + echo-typed paths | Cross-layer dependency annotated in `PRESERVATION-DESIGN.md §5.1`. The four prerequisite slices (1, 2, 3a, 3b, 3c) all landed; `preservation_l3` is the capstone. |
+| ✅ State and prove `preservation_l3` | Per-layer preservation theorem against the L3 invariants for the new echo-emitting step rules + echo-typed paths | done 2026-05-27 (L3 wiring slice 4 — capstone). Two per-case Qed lemmas (`preservation_l3_region_active_echo` for `S_Region_Exit_Echo` × `T_Region_Active_L1_Echo`, and `preservation_l3_drop_echo` for `S_Drop_Echo` × `T_Drop_L1_Echo`) plus an umbrella `preservation_l3` (their conjunction, Qed). Zero new admits or axioms. Per-case alignment forced by `T_Echo_L1`'s witness-type premise; non-deterministic crossover cases are non-preserving by design (typing derivation pins the path). Conditionally Qed under the pre-existing `region_shrink_preserves_typing_l1_gen_m` L1 structural admit per PRESERVATION-DESIGN.md §5.1. |
 
 ### Mid-term (L4 — not started)
 
@@ -226,12 +226,37 @@ to the owner**:
 | `formal/Typing.v` (legacy) | n/a | 0 | 🛑 archaeology — `Counterexample.v` depends on falsity |
 | `formal/Counterexample.v` | **5** | 0 | ✅ pinned regression witness |
 | `formal/TypingL1.v` | **2** | 0 | ✅ active — L1 judgment, modality-indexed |
-| `formal/Semantics_L1.v` | **23** | **3** | ✅ active — bullet-structure regressions + subst_typing_gen_l1_m + region_shrink_preserves_typing_l1_gen_m closed 2026-05-27; 3 residual admits are deeper L2-β debt (region_shrink T_Region_Active_L1 list-vs-multiset case now isolated in _gen_m internal admit, region_liveness_at_split narrow admit per ERegion counterexample, preservation_l1 cap) |
+| `formal/Semantics_L1.v` | **26** | **3** | ✅ active — bullet-structure regressions + subst_typing_gen_l1_m + region_shrink_preserves_typing_l1_gen_m closed 2026-05-27; 3 residual outer `Admitted.` markers cover 5 internal `admit.` cases — all pre-existing L1 structural debt OR true parallel mirrors (T_Region_Active_*_L1_Echo shadowed sub-cases mirror T_Region_Active_L1's debt; the avoidable T_Region_L1_Echo mirror was closed in slice 4). Slice 4 added 3 new Qed: `preservation_l3_region_active_echo`, `preservation_l3_drop_echo`, `preservation_l3` (umbrella). Zero new admits. |
 | `formal/Modality.v` | **1** | 0 | ✅ active — L2 core, zero axioms |
 | `formal/Echo.v` | **12** | 0 | ✅ active — L3 calculus, not yet wired into L1 |
 | `formal/TypingL2.v` | (wrapper) | (wrapper) | ✅ thin re-indexing through `TypingL1.has_type_l1` |
 | `src/abi/Ephapax/…` (Idris2) | n/a | n/a | ✅ active — ABI, Region linearity, no `believe_me` / `sorry` / `assert_total` |
 
+### Seam audit (slice 4, 2026-05-27): every admit/axiom classified
+
+Every `admit.` and `Admitted.` in `formal/*.v` after L3 slice 4
+landed. No new debt was introduced; the avoidable T_Region_L1_Echo
+mirror was closed. The remaining set is exactly the **pre-existing
+L1 structural debt** (with two true parallel mirrors that close
+when their originals close) plus the **sacrosanct legacy
+preservation** (provably false per `Counterexample.v`).
+
+| Location | Class | Closes when |
+|---|---|---|
+| `Semantics_L1.v:553` (`admit.`) | **Pre-existing** L1 structural — `region_shrink_preserves_typing_l1_gen_m` / T_Region_Active_L1 shadowed sub-case; list-vs-multiset gap | L1 perm/multiset bridge OR `T_Region_*_L1` redesign |
+| `Semantics_L1.v:621` (`admit.`) | **Parallel mirror** of `:553` — T_Region_Active_L1_Echo shadowed sub-case; structurally identical | Same as `:553` (mechanical replay) |
+| `Semantics_L1.v:653` (`Admitted.`) | **Outer marker** — depends on internal `:553` + `:621` | When both internal admits close |
+| `Semantics_L1.v:1256` (`admit.`) | **Pre-existing** L1 structural — `region_liveness_at_split_l1_gen` / T_Region_Active_L1 `r = rv` sub-case; "GENUINELY FALSE" counterexample documented at site | L2 effect-typed `TFun` per `PRESERVATION-DESIGN.md §5.1` |
+| `Semantics_L1.v:1276` (`admit.`) | **Parallel mirror** of `:1256` — T_Region_Active_L1_Echo `r = rv` sub-case | Same as `:1256` (mechanical replay) |
+| `Semantics_L1.v:1290` (`Admitted.`) | **Outer marker** — depends on internal `:1256` + `:1276` | When both internal admits close |
+| `Semantics_L1.v:1694` (`admit.`) | **Pre-existing** — `preservation_l1` body; lambda-rigidity gap per `PRESERVATION-DESIGN.md §4.8` | L2 effect-typed `TFun` (Phase 2) |
+| `Semantics_L1.v:1695` (`Admitted.`) | **Outer marker** — depends on internal `:1694` | When `:1694` closes |
+| `Semantics.v:9257` (`Admitted.`) | **🛑 Sacrosanct** — legacy `Theorem preservation`, **provably false** per `Counterexample.v` (owner directive 2026-05-27) | Never. The `Admitted.` is correct. |
+
+No `Axiom` declarations in `formal/*.v`. Counterexample.v carries 5
+Qed; TypingL1.v / Modality.v / Echo.v / TypingL2.v are all
+admit-free.
+
 ### Idris2 side (proof carriers, not Coq mechanisation)
 
 | Concern | File(s) | Status |

formal/Semantics_L1.v

@@ -564,18 +564,74 @@ Proof.
       * exact H0.
       * apply remove_first_preserves_other; [intro Hbad; apply Heq; exact Hbad | exact H1].
       * eapply IHHt. exact Hfree.
-  - (* T_Region_L1_Echo — same structural shape as T_Region_L1; the
-       proof is identical modulo the output-type [TEcho T] vs [T].
-       Both subcases (shadowed + descend) follow the original's
-       analysis. Admitted here as the outer lemma is already
-       [Admitted] and the structural residual (shadowed sub-case in
-       T_Region_Active_L1_Echo) bridges the same list-vs-multiset
-       gap documented above. *)
-    admit.
-  - (* T_Region_Active_L1_Echo — parallels T_Region_Active_L1
-       including the residual structural admit in the shadowed
-       sub-case (PROOF-NEEDS.md §2). *)
-    admit.
+  - (* T_Region_L1_Echo — structurally identical to T_Region_L1
+       modulo the output-type [TEcho T] vs [T]. Both subcases close
+       directly (shadowed via count-monotonicity vacuity, descend
+       via remove_first/remove_first_L1 commutation). Closed in
+       slice 4 to honor the "no parallel-rule admit-debt" seam-audit
+       directive — the original T_Region_L1 case has zero admits,
+       so its mirror has zero admits too. *)
+    destruct (String.eqb rr r) eqn:Heq.
+    + (* rr = r: shadowed. *)
+      apply String.eqb_eq in Heq. subst r.
+      rewrite (remove_first_not_in_id _ _ H).
+      destruct (in_dec string_dec rr (remove_first_L1 rr R_body)) as [Hin | Hnotin].
+      * (* Multiple rr's in R_body — VACUOUS by count monotonicity. *)
+        exfalso.
+        pose proof (count_occ_le_l1_m _ _ _ _ _ _ _ Ht rr) as Hle.
+        unfold cnt in Hle. simpl in Hle.
+        destruct (string_dec rr rr) as [_|Hbad]; [|apply Hbad; reflexivity].
+        apply (count_occ_In string_dec) in Hin.
+        pose proof (remove_first_L1_count_eq_self rr R_body) as Hself.
+        unfold cnt in Hself. rewrite Hself in Hin.
+        apply (count_occ_not_In string_dec) in H.
+        lia.
+      * (* At most one rr in R_body. *)
+        rewrite (remove_first_not_in_id _ _ Hnotin).
+        eapply T_Region_L1_Echo; eauto.
+    + (* rr <> r: descend. *)
+      apply String.eqb_neq in Heq.
+      assert (Hgoal_eq : remove_first rr (remove_first_L1 r R_body) =
+                        remove_first_L1 r (remove_first rr R_body)).
+      { rewrite (remove_first_eq_l1 r R_body).
+        rewrite (remove_first_eq_l1 r (remove_first rr R_body)).
+        apply remove_first_comm. }
+      rewrite Hgoal_eq.
+      eapply T_Region_L1_Echo.
+      * intro Hin. apply H. eapply remove_first_subset; exact Hin.
+      * exact H0.
+      * apply remove_first_preserves_other; [intro Hbad; apply Heq; exact Hbad | exact H1].
+      * specialize (IHHt rr Hfree).
+        simpl in IHHt.
+        destruct (String.eqb rr r) eqn:Heq2.
+        -- exfalso. apply String.eqb_eq in Heq2. apply Heq. exact Heq2.
+        -- exact IHHt.
+  - (* T_Region_Active_L1_Echo — parallels T_Region_Active_L1.
+       The descend sub-case closes directly; the shadowed sub-case
+       (rr = r) is the same list-vs-multiset structural residual as
+       in T_Region_Active_L1 above. Per slice 4 seam audit: the
+       shadowed sub-case admit is a TRUE MIRROR of the pre-existing
+       L1 structural admit at line 553. The descend sub-case is
+       closed Qed-style in slice 4 (not an admit). *)
+    destruct (String.eqb rr r) eqn:Heq.
+    + (* rr = r: shadowed — list-vs-multiset mirror of line 553.
+         Resolution path is identical to its non-Echo counterpart:
+         option (a) L1 perm lemma, (b) multiset reformulation, or
+         (c) T_Region_*_L1 redesign. See line 542-552 design note. *)
+      admit.
+    + (* rr <> r: descend. *)
+      apply String.eqb_neq in Heq.
+      assert (Hgoal_eq : remove_first rr (remove_first_L1 r R_body) =
+                        remove_first_L1 r (remove_first rr R_body)).
+      { rewrite (remove_first_eq_l1 r R_body).
+        rewrite (remove_first_eq_l1 r (remove_first rr R_body)).
+        apply remove_first_comm. }
+      rewrite Hgoal_eq.
+      eapply T_Region_Active_L1_Echo.
+      * apply remove_first_preserves_other; [intro Hbad; apply Heq; exact Hbad | exact H].
+      * exact H0.
+      * apply remove_first_preserves_other; [intro Hbad; apply Heq; exact Hbad | exact H1].
+      * eapply IHHt. exact Hfree.
   - (* T_Borrow_L1 *)
     eapply T_Borrow_L1. exact H.
   - (* T_Borrow_Val_L1 *)
@@ -1637,3 +1693,129 @@ Proof.
   intros m mu R e mu0 R0 e0 Hstep G T R_final G_out Ht.
   admit.
 Admitted.
+
+(** ** L3 preservation theorem (slice 4 of L3 wiring — capstone)
+
+    Per-layer preservation theorem for the two L3-specific
+    echo-emitting step rules [S_Region_Exit_Echo] and [S_Drop_Echo]
+    (Semantics.v slice 3c) paired with their matching L3 typing
+    rules [T_Region_Active_L1_Echo] / [T_Drop_L1_Echo] +
+    [T_Echo_L1] for the result (TypingL1.v slices 2 / 3a / 3b).
+
+    Stated as two per-case lemmas + an umbrella theorem
+    [preservation_l3] which is their conjunction.
+
+    Design constraint (PRESERVATION-DESIGN.md §6.3 +
+    PROOF-NEEDS.md §2): the L3 step rules are universally
+    quantified over the witness type [T] in the [EEcho T v]
+    residue. The non-determinism is resolved at the typing-
+    derivation level — each L3 typing rule pins [T] to its body
+    type. The per-case lemmas state preservation for the
+    matching (typing-rule, step-rule) pairs only; "cross-path"
+    pairs (e.g. legacy [T_Region_Active_L1] + L3
+    [S_Region_Exit_Echo]) are non-preserving by design and not
+    well-typed at the umbrella's [TEcho T] output.
+
+    Per CLAUDE.md owner directive 2026-05-27, slice 4:
+      - introduces ZERO new [Admitted.] or [Axiom] declarations;
+      - does NOT patch legacy [Semantics.v] preservation;
+      - re-uses already-proved infrastructure
+        ([value_R_G_preserving_l1] Qed,
+         [region_shrink_preserves_typing_l1_gen_m] — admitted at
+         the L1 layer for the T_Region_Active_L1 shadowed
+         sub-case; cross-layer dependency annotated in
+         PRESERVATION-DESIGN.md §5.1).
+
+    Cross-layer accounting: the [region_shrink_preserves_typing_l1_gen_m]
+    dependency is a pre-existing L1 structural admit (closes at
+    L2-effect-typed-TFun per design doc §5.1). Slice 4 does NOT
+    widen, duplicate, or open it — preservation_l3 is
+    *conditionally* Qed under that pre-existing L1 obligation. *)
+
+(** *** Case 1: [S_Region_Exit_Echo] paired with
+    [T_Region_Active_L1_Echo].
+
+    The typing premise extracts the body's typing
+    [R; G |=L1[m] v : T -| R_body; G']; since [v] is a value,
+    [value_R_G_preserving_l1] forces [R_body = R] and [G' = G].
+    Region shrinkage then provides the post-step witness typing
+    at [remove_first r R], and [T_Echo_L1] wraps it. *)
+
+Lemma preservation_l3_region_active_echo :
+  forall m R G r v T R_body G',
+    (* T_Region_Active_L1_Echo premises *)
+    In r R ->
+    ~ In r (Typing.free_regions T) ->
+    has_type_l1 m R G v T R_body G' ->
+    (* S_Region_Exit_Echo premises *)
+    is_value v ->
+    expr_free_of_region r v ->
+    (* Conclusion: post-step types at [TEcho T] *)
+    has_type_l1 m (remove_first r R) G
+      (EEcho T v) (TEcho T) (remove_first_L1 r R_body) G'.
+Proof.
+  intros m R G r v T R_body G' HinR HnotT Htbody Hv Hfree.
+  (* Value-invariance: R_body = R and G' = G. *)
+  pose proof (value_R_G_preserving_l1 _ _ _ _ _ _ _ Hv Htbody)
+    as [HR HG].
+  subst R_body G'.
+  (* Bridge [remove_first_L1] (typing-side) to [remove_first]
+     (semantics-side) — both pointwise equal by
+     [remove_first_eq_l1] (Qed). *)
+  replace (remove_first_L1 r R) with (remove_first r R)
+    by (symmetry; apply remove_first_eq_l1).
+  (* Goal: (remove_first r R); G |- EEcho T v : TEcho T
+                              -| (remove_first r R); G *)
+  apply T_Echo_L1; [ exact Hv | ].
+  (* Goal: (remove_first r R); G |- v : T
+                              -| (remove_first r R); G
+     This is exactly region shrinkage at [v] (free of [r]). *)
+  apply (region_shrink_preserves_typing_l1_gen_m m _ _ _ _ _ _ Htbody _ Hfree).
+Qed.
+
+(** *** Case 2: [S_Drop_Echo] paired with [T_Drop_L1_Echo].
+
+    The typing premise extracts
+    [R; G |=L1[m] ELoc l r : T -| R'; G']. Since [ELoc l r] is
+    a value (VLoc), value-invariance forces [R' = R] and
+    [G' = G]. Then [T_Echo_L1] applies directly — no region
+    shrinkage needed (step does not change [R]). *)
+
+Lemma preservation_l3_drop_echo :
+  forall m R G l r T R' G',
+    (* T_Drop_L1_Echo premises *)
+    is_linear_ty T = true ->
+    has_type_l1 m R G (ELoc l r) T R' G' ->
+    (* Conclusion: post-step types at [TEcho T] *)
+    has_type_l1 m R G (EEcho T (ELoc l r)) (TEcho T) R' G'.
+Proof.
+  intros m R G l r T R' G' Hlin Htbody.
+  pose proof (value_R_G_preserving_l1 _ _ _ _ _ _ _
+                (VLoc l r) Htbody) as [HR HG].
+  subst R' G'.
+  apply T_Echo_L1; [ apply VLoc | exact Htbody ].
+Qed.
+
+(** *** Umbrella: [preservation_l3] is the conjunction of the
+    two per-case lemmas above. Each conjunct corresponds to one
+    (L3 typing rule, L3 step rule) matched pair. *)
+
+Theorem preservation_l3 :
+  (forall m R G r v T R_body G',
+      In r R ->
+      ~ In r (Typing.free_regions T) ->
+      has_type_l1 m R G v T R_body G' ->
+      is_value v ->
+      expr_free_of_region r v ->
+      has_type_l1 m (remove_first r R) G
+        (EEcho T v) (TEcho T) (remove_first_L1 r R_body) G')
+  /\
+  (forall m R G l r T R' G',
+      is_linear_ty T = true ->
+      has_type_l1 m R G (ELoc l r) T R' G' ->
+      has_type_l1 m R G (EEcho T (ELoc l r)) (TEcho T) R' G').
+Proof.
+  split.
+  - exact preservation_l3_region_active_echo.
+  - exact preservation_l3_drop_echo.
+Qed.