feat(L1): Phase D slice 4 Phase 2 — subst_typing_gen_l1_m_ground_nonlinear + helpers (#220)

## Summary

Phase 2 of the non-linear substitution-lemma generalisation per
[`formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md`](https://github.com/hyperpolymath/ephapax/blob/main/formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md)
§"Phase 2". Builds on Phase 1's `ground_nonlinear_retype_l1_m` (#219).

Adds three pieces of NEW infrastructure to `formal/Semantics_L1.v`, all
orthogonal to legacy preservation in `Semantics.v`:

### 1. Phase 1 generalisation

`ground_nonlinear_retype_l1_m` extended from (m monomorphic, G
monomorphic) to (m → m', G → G')-polymorphic. The 3 ground typing rules
(`T_Unit_L1` / `T_Bool_L1` / `T_I32_L1`) are themselves polymorphic in
both, so the proof is unchanged. Phase 2 needs the cross-modality bridge
to lift the Linear-typed `Hv_type` into the active modality m inside the
substitution lemma's compound cases.

### 2. `ground_nonlinear_value_shift_id_l1` helper

Ground non-linear values (`EUnit` / `EBool b` / `EI32 n`) are closed
terms, so de Bruijn `shift c d v = v` for any c, d. Used to rewrite away
the `shift 0 1 vv` that `subst` introduces when descending through term
binders.

### 3. `subst_typing_gen_l1_m_ground_nonlinear` parallel lemma

```coq
forall m R Gin e T R' Gout,
  has_type_l1 m R Gin e T R' Gout ->
  forall k T1 v u_in,
    nth_error Gin k = Some (T1, u_in) ->
    is_value v ->
    is_ground_nonlinear_ty T1 = true ->
    R; remove_at k Gin |=L1 v : T1 -| R; remove_at k Gin ->
    forall u_out,
      nth_error Gout k = Some (T1, u_out) ->
      has_type_l1 m R (remove_at k Gin) (subst k v e) T R' (remove_at k Gout).
```

Mirrors `subst_typing_gen_l1_m`'s 28+ case structure. Three key
divergences from the linear lemma:

- **T_Var_Lin_L1 with `i = k0`**: rule's `is_linear_ty T = true` premise
contradicts `is_ground_nonlinear_ty Tsub = true` (discharged via
`exfalso`).
- **T_Var_Unr_L1 with `i = k0`**: CONSTRUCTIVE here (the symmetric case
in the linear lemma is the exfalso branch). The substituted value `vv`
is lifted from Linear into the active modality m via
`ground_nonlinear_retype_l1_m`.
- **Compound rules**: `ground_nonlinear_retype_l1_m` replaces the
`linear_value_is_loc_l1` + `loc_retype_at_R_l1_m` +
`region_liveness_at_split_l1_gen` pipeline. The retype takes any R', G',
m', so no liveness side-condition is required.

## Why this matters

Phase 2 unblocks:
- **Phase 3**: `tfuneff_lambda_retype_l1_m` + extend substitution to
`TFunEff T1` lambdas.
- **Phase 4**: close `preservation_l2`'s `T_App_L2_Eff` β-case for
ground non-linear `T1` (in `TFunEff T1 T2 R_in R_out` lambdas with `T1 ∈
{TBase TUnit, TBase TBool, TBase TI32}`).

Ships as a **sibling lemma** rather than folding case-split into the
existing `subst_typing_gen_l1_m` to preserve the ~30 Qed downstreams.

## Owner-directive compliance

Per `CLAUDE.md` 2026-05-27:

- Does NOT close `Theorem preservation` in `Semantics.v`.
- Does NOT extend `Semantics.v` / `Typing.v` / `Counterexample.v` (all
untouched).
- Does NOT close residual `Semantics_L1.v` admits via this work —
strictly NEW infrastructure.
- Adds no new `Axiom` or `Admitted` declarations.

## Test plan

- [x] `just clean && just all` in `formal/` — clean rebuild of all 10
`.v` files (coqc 8.18.0).
- [x] Zero new admits/axioms (all proofs `Qed`).
- [x] `Semantics.v`/`Typing.v`/`Counterexample.v` untouched.
- [x] GPG-signed commit.
- [x] STATE.a2ml `next_action` shifted to Phase 3.

## Diff

- `formal/Semantics_L1.v` +322 (lemma + 2 helpers + doc comments)
- `.machine_readable/6a2/STATE.a2ml` +1/-1 (state journal advance)

## Refs

Refs hyperpolymath/standards#134 (sub-issue of
hyperpolymath/standards#124 estate proof-debt epic). Follows #219 (Phase
1). Phase 3 (TFunEff lambda retype) is the next slice.

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

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -6,8 +6,8 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Phase D slice 4 Phase 2 — ship `subst_typing_gen_l1_m_ground_nonlinear` per `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md` §'Phase 2'. Parallel substitution lemma for ground non-linear `T1` (TBase TUnit / TBase TBool / TBase TI32). Structure mirrors the existing `subst_typing_gen_l1_m` 28-case induction at `formal/Semantics_L1.v:1358`. Key divergences: (i) `T_Var_Lin_L1` with `i = k0` discharges via `is_linear_ty T1 = false` vs T_Var_Lin_L1's `is_linear_ty T = true` premise (exfalso); (ii) `T_Var_Unr_L1` with `i = k0` becomes a CONSTRUCTIVE case — apply `Hv_type` directly (in the existing lemma this is vacuous via `Hlin`); (iii) compound cases use `ground_nonlinear_retype_l1_m` (NEW — Phase 1, landed in PR #219) in place of `loc_retype_at_R_l1_m` for R-shift retypes. Estimated ~250-300 lines paralleling existing proof. Ships as sibling lemma (NOT case-split into existing one) to avoid breaking ~30 Qed downstreams of `subst_typing_gen_l1_m`. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted` to close cases; no touching `Semantics.v`/`Typing.v`/`Counterexample.v`; no closure of residual `Semantics_L1.v` admits via this work — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
-last_action: "Phase D slice 4 Phase 1 LANDED (2026-05-30): `is_ground_nonlinear_ty` predicate added to `formal/Syntax.v` (after `is_linear_ty`); `ground_nonlinear_retype_l1_m` lemma added to `formal/Semantics_L1.v` (after `loc_retype_at_R_l1_m`). Signature: `forall m R R' G v T, is_value v → is_ground_nonlinear_ty T = true → has_type_l1 m R G v T R G → has_type_l1 m R' G v T R' G`. Proof: destruct on `is_value v` witness; in EUnit/EBool/EI32 cases invert typing and re-apply T_Unit_L1/T_Bool_L1/T_I32_L1 at R'; in non-ground value cases (ELam/EPair/EInl/EInr/ELoc/EBorrow/EEcho) every typing-rule inversion gives a non-ground T discriminated by Hgrd. Total addition: ~30 lines in Semantics_L1.v + ~12 lines in Syntax.v. Coqc 8.18.0 clean across all 10 .v files. Zero new admits/axioms. `Semantics.v`/`Typing.v`/`Counterexample.v` untouched. Unblocks Phase 2 (parallel substitution lemma for ground non-linear T1). PR #219."
+next_action: "Phase D slice 4 Phase 3 — ship `tfuneff_lambda_retype_l1_m` per `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md` §'Phase 3'. Retype lemma for TFunEff-typed lambdas (`ELam T0 e` typed at `TFunEff T1 T2 R_in R_out`) under the side condition `forall r, In r R' -> In r R_in`. Extend the Phase 2 substitution lemma to cover `T1 = TFunEff …` lambdas as substituends. The TFun (non-Eff) lambda case has body-R-rigidity (same gap as legacy preservation_l1 slice 4b) — explicitly OUT OF SCOPE for Phase 3 per design doc §'Open design questions' #2 (recommended: TFunEff only). After Phase 3, Phase 4 closes `preservation_l2`'s `T_App_L2_Eff` β-case for: (a) linear T1 via existing `subst_typing_gen_l1_m`; (b) ground non-linear T1 via Phase 2's `subst_typing_gen_l1_m_ground_nonlinear`; (c) TFunEff non-linear T1 via Phase 3; (d) compound non-linear T1 deferred to Phase 5. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted` to close cases; no touching `Semantics.v`/`Typing.v`/`Counterexample.v`; no closure of residual `Semantics_L1.v` admits via this work — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
+last_action: "Phase D slice 4 Phase 2 LANDED (2026-05-30): `subst_typing_gen_l1_m_ground_nonlinear` parallel substitution lemma added to `formal/Semantics_L1.v` mirroring `subst_typing_gen_l1_m`'s 28+ case structure for `is_ground_nonlinear_ty T1 = true`. Three key divergences from the linear lemma: (i) T_Var_Lin_L1 i=k0 → exfalso via `is_linear_ty Tsub = false` vs rule's premise `is_linear_ty T = true`; (ii) T_Var_Unr_L1 i=k0 → CONSTRUCTIVE case applying `ground_nonlinear_retype_l1_m` to lift Hv_type from Linear to active modality m; (iii) compound rules use `ground_nonlinear_retype_l1_m` directly (no `linear_value_is_loc_l1` / `loc_retype_at_R_l1_m` / `region_liveness_at_split_l1_gen` pipeline — ground retype takes any R, any G, any m). Phase 1's `ground_nonlinear_retype_l1_m` generalised in this PR to (m → m', R → R', G → G')-polymorphic (Phase 1 ships m-monomorphic R-only retype; Phase 2 needs the cross-modality cross-context bridge). New helper `ground_nonlinear_value_shift_id_l1` proves `shift c d v = v` for ground non-linear values; used to rewrite the `shift 0 1 vv` introduced by `subst`'s descent through term binders in T_Let_L1 / T_LetLin_L1 / T_Lam_L1_* (4 lambda rules) / T_Case_L1_* (2 case rules). Coqc 8.18.0 clean rebuild across all 10 .v files. Zero new admits/axioms. `Semantics.v`/`Typing.v`/`Counterexample.v` untouched. Phase 2 unblocks Phase 3 (TFunEff lambda retype) and Phase 4 (close preservation_l2 β-case for ground non-linear T1). Sibling-lemma approach preserves ~30 Qed downstreams of `subst_typing_gen_l1_m`."
 updated: 2026-05-30T00:00:00Z
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):

formal/Semantics_L1.v

@@ -1197,13 +1197,13 @@ Proof. intros. apply T_Loc_L1. assumption. Qed.
     [has_type_l1] judgment carrying the modality parameter [m]. It
     does not extend or patch [Semantics.v]. *)
 Lemma ground_nonlinear_retype_l1_m :
-  forall (m : Modality) (R R' : region_env) (G : ctx) (v : expr) (T : ty),
+  forall (m m' : Modality) (R R' : region_env) (G G' : ctx) (v : expr) (T : ty),
     is_value v ->
     is_ground_nonlinear_ty T = true ->
     has_type_l1 m R G v T R G ->
-    has_type_l1 m R' G v T R' G.
+    has_type_l1 m' R' G' v T R' G'.
 Proof.
-  intros m R R' G v T Hval Hgrd Ht.
+  intros m m' R R' G G' v T Hval Hgrd Ht.
   destruct Hval as
     [ | b | n
     | T0 e0 | v1 v2 Hv1 Hv2
@@ -1217,6 +1217,37 @@ Proof.
   - (* v = EI32 n, T = TBase TI32 *) apply T_I32_L1.
 Qed.
 
+(** Ground non-linear values are closed terms — they contain no
+    de Bruijn variables, so de Bruijn [shift] is the identity on them.
+
+    Used by [subst_typing_gen_l1_m_ground_nonlinear] under term-binder
+    cases (T_Let_L1, T_LetLin_L1, the four T_Lam_L1 lambda rules, and
+    the two T_Case_L1 case rules), where the operational substitution
+    introduces a [shift 0 1 vv] around the substituted value when
+    descending through a binder. For ground non-linear [vv]
+    (EUnit / EBool b / EI32 n) the shift is definitionally the
+    identity; this lemma packages that observation so the rewrite can
+    fire after canonical-form extraction.
+
+    Refs [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md] Phase 2. *)
+Lemma ground_nonlinear_value_shift_id_l1 :
+  forall m R G v T c d,
+    is_value v ->
+    is_ground_nonlinear_ty T = true ->
+    has_type_l1 m R G v T R G ->
+    shift c d v = v.
+Proof.
+  intros m R G v T c d Hval Hgrd Ht.
+  destruct Hval as
+    [ | b | n
+    | T0 e0 | v1 v2 Hv1 Hv2
+    | T0 v0 Hv0 | T0 v0 Hv0
+    | l r
+    | v0 Hv0
+    | T0 v0 Hv0 ];
+    inversion Ht; subst; try discriminate Hgrd; reflexivity.
+Qed.
+
 (** Narrower axiom (region-liveness at compound-rule split points).
 
     Given a well-typed sub-derivation [R; G |=L1 e1 : T1 -| R1; G']
@@ -1695,6 +1726,292 @@ Proof.
   - eapply T_Observe_L1. eapply IHHtype; eassumption.
 Qed.
 
+(** Parallel substitution lemma for ground non-linear [T1].
+
+    Phase D slice 4 Phase 2 per [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md].
+    Mirrors [subst_typing_gen_l1_m] structurally; the case-internal
+    reasoning differs in three places:
+
+    - [T_Var_Lin_L1] with [i = k0]: the rule's [is_linear_ty T = true]
+      premise contradicts [Hgrd : is_ground_nonlinear_ty Tsub = true]
+      (since [is_ground_nonlinear_ty Tsub = true ->
+      is_linear_ty Tsub = false] by inspection). Discharged via
+      [exfalso].
+    - [T_Var_Unr_L1] with [i = k0]: CONSTRUCTIVE here (the symmetric
+      case in the linear lemma is the exfalso branch). The substituted
+      value [vv] typed at [Linear] is lifted to the active modality [m]
+      via [ground_nonlinear_retype_l1_m] (Phase 1).
+    - Compound rules: [ground_nonlinear_retype_l1_m] replaces the
+      [linear_value_is_loc_l1] + [loc_retype_at_R_l1_m] +
+      [region_liveness_at_split_l1_gen] pipeline. The retype takes any
+      [R'], so no liveness side-condition is required.
+
+    Ships as a SIBLING lemma rather than folding case-split into the
+    existing [subst_typing_gen_l1_m] to preserve the ~30 [Qed]
+    downstreams. *)
+Lemma subst_typing_gen_l1_m_ground_nonlinear :
+  forall m R Gin e T R' Gout,
+    has_type_l1 m R Gin e T R' Gout ->
+    forall k T1 v u_in,
+      nth_error Gin k = Some (T1, u_in) ->
+      is_value v ->
+      is_ground_nonlinear_ty T1 = true ->
+      R; remove_at k Gin |=L1 v : T1 -| R; remove_at k Gin ->
+      forall u_out,
+        nth_error Gout k = Some (T1, u_out) ->
+        has_type_l1 m R (remove_at k Gin) (subst k v e) T R' (remove_at k Gout).
+Proof.
+  intros m R Gin e T R' Gout Htype.
+  induction Htype; intros k0 Tsub vv u_in Hk_in Hval Hgrd Hv_type u_out Hk_out; simpl.
+
+  (* T_Unit_L1, T_Bool_L1, T_I32_L1 *)
+  1-3: (assert (u_out = u_in) by congruence; subst; constructor).
+
+  (* T_Var_Lin_L1 *)
+  - destruct (Nat.eq_dec i k0) as [->|Hne].
+    + (* i = k0: rule's [is_linear_ty T = true] contradicts
+         [is_ground_nonlinear_ty Tsub = true] *)
+      exfalso.
+      assert (T = Tsub) by (unfold ctx_lookup in H; congruence). subst T.
+      destruct Tsub as [b| | | | | | | | |]; try discriminate Hgrd.
+      destruct b; try discriminate Hgrd; discriminate H0.
+    + rewrite (proj2 (Nat.eqb_neq i k0) Hne).
+      destruct (Nat.ltb_spec k0 i) as [Hlt|Hge].
+      * assert (Hrw: remove_at k0 (ctx_mark_used G i) =
+                     ctx_mark_used (remove_at k0 G) (i - 1)).
+        { replace i with (S (i - 1)) at 1 by lia.
+          apply remove_at_ctx_mark_used_gt. lia. }
+        rewrite Hrw.
+        eapply T_Var_Lin_L1.
+        -- unfold ctx_lookup. rewrite nth_error_remove_at_ge by lia.
+           replace (S (i - 1)) with i by lia.
+           unfold ctx_lookup in H. exact H.
+        -- exact H0.
+      * assert (i < k0) by lia.
+        rewrite remove_at_ctx_mark_used_lt by lia.
+        eapply T_Var_Lin_L1.
+        -- unfold ctx_lookup. rewrite nth_error_remove_at_lt by lia.
+           unfold ctx_lookup in H. exact H.
+        -- exact H0.
+
+  (* T_Var_Unr_L1 *)
+  - destruct (Nat.eq_dec i k0) as [->|Hne].
+    + (* i = k0: CONSTRUCTIVE case for ground non-linear substitution.
+         Rule output context equals input — no marking. *)
+      rewrite Nat.eqb_refl.
+      assert (T = Tsub) by (unfold ctx_lookup in H; congruence). subst T.
+      assert (u_out = u_in) by congruence; subst u_out.
+      eapply ground_nonlinear_retype_l1_m; eauto.
+    + rewrite (proj2 (Nat.eqb_neq i k0) Hne).
+      destruct (Nat.ltb_spec k0 i) as [Hlt|Hge].
+      * eapply T_Var_Unr_L1.
+        -- unfold ctx_lookup. rewrite nth_error_remove_at_ge by lia.
+           replace (S (i - 1)) with i by lia.
+           unfold ctx_lookup in H. exact H.
+        -- exact H0.
+      * assert (i < k0) by lia. eapply T_Var_Unr_L1.
+        -- unfold ctx_lookup. rewrite nth_error_remove_at_lt by lia.
+           unfold ctx_lookup in H. exact H.
+        -- exact H0.
+
+  (* T_Loc_L1 *)
+  - assert (u_out = u_in) by congruence; subst. constructor. assumption.
+  (* T_StringNew_L1 *)
+  - assert (u_out = u_in) by congruence; subst. constructor. assumption.
+
+  (* T_StringConcat_L1 *)
+  - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid].
+    eapply T_StringConcat_L1.
+    + eapply IHHtype1; eassumption.
+    + eapply IHHtype2; try eassumption; try reflexivity.
+      eapply ground_nonlinear_retype_l1_m; eauto.
+
+  (* T_StringLen_L1 *)
+  - eapply T_StringLen_L1. eapply IHHtype; eassumption.
+
+  (* T_Let_L1 *)
+  - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid].
+    eapply T_Let_L1.
+    + eapply IHHtype1; eassumption.
+    + rewrite (ground_nonlinear_value_shift_id_l1 _ _ _ _ _ 0 1 Hval Hgrd Hv_type).
+      eapply (IHHtype2 (S k0) Tsub vv u_mid);
+        simpl; try eassumption; try reflexivity.
+      eapply ground_nonlinear_retype_l1_m; eassumption.
+
+  (* T_LetLin_L1 *)
+  - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid].
+    eapply T_LetLin_L1; [exact H | |].
+    + eapply IHHtype1; eassumption.
+    + rewrite (ground_nonlinear_value_shift_id_l1 _ _ _ _ _ 0 1 Hval Hgrd Hv_type).
+      eapply (IHHtype2 (S k0) Tsub vv u_mid);
+        simpl; try eassumption; try reflexivity.
+      eapply ground_nonlinear_retype_l1_m; eassumption.
+
+  (* T_Lam_L1_Linear: body's R = outer R; ground value retypes trivially. *)
+  - assert (u_out = u_in) by congruence; subst.
+    eapply T_Lam_L1_Linear.
+    rewrite (ground_nonlinear_value_shift_id_l1 _ _ _ _ _ 0 1 Hval Hgrd Hv_type).
+    eapply (IHHtype (S k0) Tsub vv u_in);
+      simpl; try eassumption; try reflexivity.
+    eapply ground_nonlinear_retype_l1_m; eassumption.
+
+  (* T_Lam_L1_Affine *)
+  - assert (u_out = u_in) by congruence; subst.
+    eapply T_Lam_L1_Affine.
+    rewrite (ground_nonlinear_value_shift_id_l1 _ _ _ _ _ 0 1 Hval Hgrd Hv_type).
+    eapply (IHHtype (S k0) Tsub vv u_in);
+      simpl; try eassumption; try reflexivity.
+    eapply ground_nonlinear_retype_l1_m; eassumption.
+
+  (* T_Lam_L1_Linear_Eff — body's R = R_in (independent of outer R);
+     ground value retypes to ANY R, so no [R -> R_in] side-condition
+     is needed. *)
+  - assert (u_out = u_in) by congruence; subst.
+    eapply T_Lam_L1_Linear_Eff; [exact H |].
+    rewrite (ground_nonlinear_value_shift_id_l1 _ _ _ _ _ 0 1 Hval Hgrd Hv_type).
+    eapply (IHHtype (S k0) Tsub vv u_in);
+      simpl; try eassumption; try reflexivity.
+    eapply ground_nonlinear_retype_l1_m; eassumption.
+
+  (* T_Lam_L1_Affine_Eff *)
+  - assert (u_out = u_in) by congruence; subst.
+    eapply T_Lam_L1_Affine_Eff; [exact H |].
+    rewrite (ground_nonlinear_value_shift_id_l1 _ _ _ _ _ 0 1 Hval Hgrd Hv_type).
+    eapply (IHHtype (S k0) Tsub vv u_in);
+      simpl; try eassumption; try reflexivity.
+    eapply ground_nonlinear_retype_l1_m; eassumption.
+
+  (* T_App_L1 *)
+  - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid].
+    eapply T_App_L1.
+    + eapply IHHtype1; eassumption.
+    + eapply IHHtype2; try eassumption; try reflexivity.
+      eapply ground_nonlinear_retype_l1_m; eauto.
+
+  (* T_Pair_L1 *)
+  - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid].
+    eapply T_Pair_L1.
+    + eapply IHHtype1; eassumption.
+    + eapply IHHtype2; try eassumption; try reflexivity.
+      eapply ground_nonlinear_retype_l1_m; eauto.
+
+  (* T_Fst_L1 *)
+  - eapply T_Fst_L1; [eapply IHHtype; eassumption | assumption].
+
+  (* T_Snd_L1 *)
+  - eapply T_Snd_L1; [eapply IHHtype; eassumption | assumption].
+
+  (* T_Inl_L1 *)
+  - eapply T_Inl_L1. eapply IHHtype; eassumption.
+
+  (* T_Inr_L1 *)
+  - eapply T_Inr_L1. eapply IHHtype; eassumption.
+
+  (* T_Case_L1_Linear *)
+  - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid].
+    eapply T_Case_L1_Linear.
+    + eapply IHHtype1; eassumption.
+    + rewrite (ground_nonlinear_value_shift_id_l1 _ _ _ _ _ 0 1 Hval Hgrd Hv_type).
+      eapply (IHHtype2 (S k0) Tsub vv u_mid);
+        simpl; try eassumption; try reflexivity.
+      eapply ground_nonlinear_retype_l1_m; eassumption.
+    + rewrite (ground_nonlinear_value_shift_id_l1 _ _ _ _ _ 0 1 Hval Hgrd Hv_type).
+      eapply (IHHtype3 (S k0) Tsub vv u_mid);
+        simpl; try eassumption; try reflexivity.
+      eapply ground_nonlinear_retype_l1_m; eassumption.
+
+  (* T_Case_L1_Affine *)
+  - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid].
+    eapply T_Case_L1_Affine.
+    + eapply IHHtype1; eassumption.
+    + rewrite (ground_nonlinear_value_shift_id_l1 _ _ _ _ _ 0 1 Hval Hgrd Hv_type).
+      eapply (IHHtype2 (S k0) Tsub vv u_mid);
+        simpl; try eassumption; try reflexivity.
+      eapply ground_nonlinear_retype_l1_m; eassumption.
+    + rewrite (ground_nonlinear_value_shift_id_l1 _ _ _ _ _ 0 1 Hval Hgrd Hv_type).
+      eapply (IHHtype3 (S k0) Tsub vv u_mid);
+        simpl; try eassumption; try reflexivity.
+      eapply ground_nonlinear_retype_l1_m; eassumption.
+
+  (* T_If_L1_Linear *)
+  - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid].
+    eapply T_If_L1_Linear.
+    + eapply IHHtype1; eassumption.
+    + eapply IHHtype2; try eassumption; try reflexivity.
+      eapply ground_nonlinear_retype_l1_m; eauto.
+    + eapply IHHtype3; try eassumption; try reflexivity.
+      eapply ground_nonlinear_retype_l1_m; eauto.
+
+  (* T_If_L1_Affine *)
+  - destruct (output_shape_at_l1 _ _ _ _ _ _ _ _ _ _ Htype1 Hk_in) as [u_mid Hu_mid].
+    eapply T_If_L1_Affine.
+    + eapply IHHtype1; eassumption.
+    + eapply IHHtype2; try eassumption; try reflexivity.
+      eapply ground_nonlinear_retype_l1_m; eauto.
+    + eapply IHHtype3; try eassumption; try reflexivity.
+      eapply ground_nonlinear_retype_l1_m; eauto.
+
+  (* T_Region_L1: body's R = [r :: R]; ground retypes trivially. *)
+  - eapply T_Region_L1; [exact H | exact H0 | exact H1 |].
+    eapply IHHtype; try eassumption; try reflexivity.
+    eapply ground_nonlinear_retype_l1_m; eauto.
+
+  (* T_Region_Active_L1 *)
+  - eapply T_Region_Active_L1; [exact H | exact H0 | exact H1 |].
+    eapply IHHtype; try eassumption; try reflexivity.
+
+  (* T_Region_L1_Echo *)
+  - eapply T_Region_L1_Echo; [exact H | exact H0 | exact H1 |].
+    eapply IHHtype; try eassumption; try reflexivity.
+    eapply ground_nonlinear_retype_l1_m; eauto.
+
+  (* T_Region_Active_L1_Echo *)
+  - eapply T_Region_Active_L1_Echo; [exact H | exact H0 | exact H1 |].
+    eapply IHHtype; try eassumption; try reflexivity.
+
+  (* T_Borrow_L1: EBorrow (EVar i) *)
+  - destruct (Nat.eq_dec i k0) as [->|Hne].
+    + simpl. rewrite Nat.eqb_refl.
+      assert (T = Tsub) by (unfold ctx_lookup in H; congruence); subst T.
+      assert (u_out = u_in) by congruence; subst.
+      eapply T_Borrow_Val_L1.
+      * (* vv is a ground value, hence a value *) assumption.
+      * eapply ground_nonlinear_retype_l1_m; eauto.
+    + simpl. rewrite (proj2 (Nat.eqb_neq i k0) Hne).
+      assert (u_out = u_in) by congruence; subst.
+      destruct (Nat.ltb_spec k0 i) as [Hlt|Hge].
+      * eapply T_Borrow_L1. unfold ctx_lookup.
+        rewrite nth_error_remove_at_ge by lia.
+        replace (S (i - 1)) with i by lia.
+        unfold ctx_lookup in H. exact H.
+      * assert (i < k0) by lia. eapply T_Borrow_L1. unfold ctx_lookup.
+        rewrite nth_error_remove_at_lt by lia.
+        unfold ctx_lookup in H. exact H.
+
+  (* T_Borrow_Val_L1 *)
+  - assert (u_out = u_in) by congruence; subst.
+    eapply T_Borrow_Val_L1.
+    + apply subst_preserves_value. assumption.
+    + eapply IHHtype; eassumption.
+
+  (* T_Drop_L1 *)
+  - eapply T_Drop_L1; [exact H |]. eapply IHHtype; eassumption.
+
+  (* T_Drop_L1_Echo *)
+  - eapply T_Drop_L1_Echo; [exact H |]. eapply IHHtype; eassumption.
+
+  (* T_Copy_L1 *)
+  - eapply T_Copy_L1; [exact H |]. eapply IHHtype; eassumption.
+
+  (* T_Echo_L1 *)
+  - eapply T_Echo_L1.
+    + apply subst_preserves_value. assumption.
+    + eapply IHHtype; eassumption.
+
+  (* T_Observe_L1 *)
+  - eapply T_Observe_L1. eapply IHHtype; eassumption.
+Qed.
+
 (** Linear-specialised wrapper preserving the original signature for
     [subst_preserves_typing_l1] and [preservation_l1]. *)
 Lemma subst_typing_gen_l1 :