fix(L1): HOTFIX — dedupe tfuneff_lambda_retype_l1_m (main is broken) (#226)

## TL;DR — P0 hotfix

\`main\` does NOT compile as of 2026-05-30 13:27:45Z. PR #224
admin-merged with auto-merge SQUASH ~7 minutes after PR #223, and both
added the same Lemma \`tfuneff_lambda_retype_l1_m\`. CI did not catch
the duplicate because the GitHub CI workflows currently exercise
governance / security scanners only — not the Coq build oracle.

Local rebuild:

\`\`\`
File "./Semantics_L1.v", line 1361, characters 6-32:
Error: tfuneff_lambda_retype_l1_m already exists.
\`\`\`

This PR removes the duplicate block (PR #224's copy, lines 1311-1382 of
post-merge file). Original (PR #223) at lines 1257-1278 is unchanged.
\`Syntax.is_tfuneff_ty\` (also added by #224) is INDEPENDENTLY useful
for Phase 3b precondition shape — preserved untouched.

## Verification

\`\`\`
$ cd /tmp/ephapax-design-amendment/formal && just all
coq_makefile -f _CoqProject -o build.mk
make -f build.mk
COQDEP VFILES
COQC Semantics_L1.v
COQC Counterexample.v
COQC Echo.v
COQC TypingL2.v
COQC L4.v
(exit 0)
\`\`\`

Rocq 9.1.1 / Coq 8.18. Zero new admits, zero new axioms, zero semantic
changes (the two duplicate lemmas were behaviorally equivalent modulo
argument order; v1 is kept as the earlier-merged canonical version).

## Net delta

- \`formal/Semantics_L1.v\`: 73 lines deleted (no insertions).

## Root-cause + follow-up

Parallel-session collision: two agent sessions both shipped Phase 3a
infrastructure within a 7-minute window without cross-checking. PR #223
merged at 13:21:06Z. PR #224 enabled auto-merge at 13:26:48Z (5min33s
after #223), so the author could not have known #223 was already merged
when arming auto-merge.

Mitigation surface for follow-up issues:
1. **Coq build oracle into CI** — currently zero gate at the
typechecking layer. ANY duplicate-Lemma / broken-proof PR will
admin-merge green. File issue to add a Coq build job to the workflow
set.
2. **Parallel-session signal** — pre-merge \`git log origin/main -5 --
formal/\` would have caught the collision. Could be a Hypatia rule on
parallel ephapax sessions.

## Owner-directive compliance

- Does NOT modify \`Semantics.v\`.
- Does NOT add new admits or axioms.
- Reverts a parallel-session collision; not a proof trick to close
legacy admits.

🤖 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

@@ -1308,79 +1308,6 @@ Proof.
     inversion Ht; subst; try discriminate Hgrd; reflexivity.
 Qed.
 
-(** TFunEff lambda retype lemma — Phase D slice 4 Phase 3 per
-    [formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md].
-
-    A [TFunEff]-typed lambda value [ELam T0 e] is formed by either
-    [T_Lam_L1_Linear_Eff] or [T_Lam_L1_Affine_Eff] (per
-    [formal/TypingL1.v]). Both rules carry the side condition
-    [forall r, In r R -> In r R_in] at the formation env [R], and
-    type the body [e] at the BODY env [R_in] (which is part of the
-    function type [TFunEff T1 T2 R_in R_out]).
-
-    The body's typing is therefore INDEPENDENT of the outer formation
-    env [R]. Re-applying the formation rule at any [R'] satisfying the
-    rule's side condition [forall r, In r R' -> In r R_in] re-derives
-    the lambda's typing at [R'] — the body typing carries over
-    unchanged.
-
-    Contrast with [ground_nonlinear_retype_l1_m] (Phase 1), which
-    retypes EUnit / EBool / EI32 across ANY [R'] without a side
-    condition (those values have no R-dependent body).
-
-    Non-ELam value forms (EUnit, EBool, EI32, EPair, EInl, EInr, ELoc,
-    EBorrow, EEcho) do not type at [TFunEff …] (their typing rules
-    produce different type shapes). Inversion closes those cases via
-    [discriminate] on the type-equation residue.
-
-    For ELam at [TFunEff …], inversion of [Ht] yields one of four
-    [T_Lam_L1_*] constructors. The two non-Eff constructors
-    ([T_Lam_L1_Linear], [T_Lam_L1_Affine]) produce [TFun T1 T2]
-    (no R_in / R_out fields), so the type-equation residue
-    [TFun … = TFunEff …] discriminates. The two Eff constructors
-    fire constructively, with re-application supplying the new R'
-    and the supplied side condition [Hsub].
-
-    Note on modality monomorphism: unlike
-    [ground_nonlinear_retype_l1_m] (which is [m -> m']-polymorphic
-    via the modality-independence of ground constructors), this
-    lemma is [m]-monomorphic. A TFunEff lambda formed via
-    [T_Lam_L1_Linear_Eff] (mode Linear) cannot be directly re-derived
-    via [T_Lam_L1_Affine_Eff] (mode Affine) without lifting the body
-    typing across the [Linear -> Affine] modality bridge (which is
-    [linear_to_affine] in [TypingL2.v], but that operates on full
-    derivations not under retype). Phase 3 does not require cross-mode
-    retype — the Phase 4 [T_App_L2_Eff] β-case uses a single fixed [m]
-    throughout. Cross-modality TFunEff retype, if ever needed, would
-    layer [linear_to_affine] over this lemma.
-
-    Orthogonal to legacy [preservation] in [Semantics.v]: this lemma
-    adds NEW infrastructure constrained to the post-redesign
-    [has_type_l1] judgment carrying the modality parameter [m]. It
-    does not extend or patch [Semantics.v]. *)
-Lemma tfuneff_lambda_retype_l1_m :
-  forall (m : Modality) (R R' : region_env) (G : ctx) (v : expr)
-         (T1 T2 : ty) (R_in R_out : region_env),
-    is_value v ->
-    (forall r, In r R' -> In r R_in) ->
-    has_type_l1 m R G v (TFunEff T1 T2 R_in R_out) R G ->
-    has_type_l1 m R' G v (TFunEff T1 T2 R_in R_out) R' G.
-Proof.
-  intros m R R' G v T1 T2 R_in R_out Hval Hsub 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.
-  - (* v = ELam T0 e0, T_Lam_L1_Linear_Eff *)
-    eapply T_Lam_L1_Linear_Eff; [exact Hsub | eassumption].
-  - (* v = ELam T0 e0, T_Lam_L1_Affine_Eff *)
-    eapply T_Lam_L1_Affine_Eff; [exact Hsub | eassumption].
-Qed.
-
 (** Narrower axiom (region-liveness at compound-rule split points).
 
     Given a well-typed sub-derivation [R; G |=L1 e1 : T1 -| R1; G']