diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 9aa124b..f0966d1 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -187,8 +187,25 @@ jobs:
     steps:
       - uses: actions/checkout@v6
 
+      # Staging override: on a PR from branch <b>, if the case-study repo has a
+      # branch named <pinned>-<b>, clone that instead of the pinned branch.
+      # Lets case studies be updated against an in-flight LemmaScript branch
+      # without touching the branch that main's CI pins.
       - name: Clone case study
-        run: git clone --branch ${{ matrix.branch }} https://github.com/${{ matrix.repo }}.git ../case-study
+        env:
+          DEFAULT_BRANCH: ${{ matrix.branch }}
+          LS_BRANCH: ${{ github.head_ref || github.ref_name }}
+        run: |
+          repo="https://github.com/${{ matrix.repo }}.git"
+          branch="$DEFAULT_BRANCH"
+          if [ "$LS_BRANCH" != "main" ]; then
+            staging="$DEFAULT_BRANCH-$LS_BRANCH"
+            if git ls-remote --exit-code --heads "$repo" "$staging" >/dev/null; then
+              echo "Using staging branch $staging (default: $DEFAULT_BRANCH)"
+              branch="$staging"
+            fi
+          fi
+          git clone --branch "$branch" "$repo" ../case-study
 
       - uses: actions/setup-node@v6
         with:
@@ -234,8 +251,25 @@ jobs:
     steps:
       - uses: actions/checkout@v6
 
+      # Staging override: on a PR from branch <b>, if the case-study repo has a
+      # branch named <pinned>-<b>, clone that instead of the pinned branch.
+      # Lets case studies be updated against an in-flight LemmaScript branch
+      # without touching the branch that main's CI pins.
       - name: Clone case study
-        run: git clone --branch ${{ matrix.branch }} https://github.com/${{ matrix.repo }}.git ../case-study
+        env:
+          DEFAULT_BRANCH: ${{ matrix.branch }}
+          LS_BRANCH: ${{ github.head_ref || github.ref_name }}
+        run: |
+          repo="https://github.com/${{ matrix.repo }}.git"
+          branch="$DEFAULT_BRANCH"
+          if [ "$LS_BRANCH" != "main" ]; then
+            staging="$DEFAULT_BRANCH-$LS_BRANCH"
+            if git ls-remote --exit-code --heads "$repo" "$staging" >/dev/null; then
+              echo "Using staging branch $staging (default: $DEFAULT_BRANCH)"
+              branch="$staging"
+            fi
+          fi
+          git clone --branch "$branch" "$repo" ../case-study
 
       - uses: actions/setup-node@v6
         with:
diff --git a/SPEC.md b/SPEC.md
index 36b04b8..60eec27 100644
--- a/SPEC.md
+++ b/SPEC.md
@@ -469,13 +469,13 @@ The same coercion applies to non-bool conditions in `if`/`while`/`?:` positions:
 | `s.length` | `s.length` | `\|s\|` |
 | `Math.max(...s)` / `Math.min(...s)` | — | `MaxOfSeq(s)` / `MinOfSeq(s)` (requires `\|s\| > 0`) |
 | `perm(a, b)` (spec-only) | — | `Perm(a, b)` (preamble: `predicate Perm<T(==)>(a, b) { multiset(a) == multiset(b) }`) |
-| `arr.map((x) => e)` | `arr.map (fun x => e)` | `Std.Collections.Seq.Map((x) => e, arr)` |
+| `arr.map((x) => e)` | `arr.map (fun x => e)` | `seq(\|arr\|, i requires 0 <= i < \|arr\| => var x := arr[i]; e)` (§3.7) |
 | `arr.filter((x) => e)` | `arr.filter (fun x => e)` | `Std.Collections.Seq.Filter((x) => e, arr)` |
 | `arr.every((x) => e)` | `arr.all (fun x => e)` | `Std.Collections.Seq.All(arr, (x) => e)` |
 | `arr.some((x) => e)` | `arr.any (fun x => e)` | `exists x :: x in arr && e` |
 | `arr.includes(x)` | `arr.contains x` | `(x in arr)` |
 | `arr.indexOf(x)` | — | `SeqIndexOf(arr, x)` (preamble) |
-| `arr.find((x) => e)` | `arr.find? (fun x => e)` | — |
+| `arr.find((x) => e)` | `arr.find? (fun x => e)` | `SeqFind(arr, (x) => e)` (preamble) |
 | `arr.findIndex((x) => e)` | — | `SeqFindIndex(arr, (x) => e)` (preamble: `-1 ⇔ no match`, `≥0 ⇔ first match with no earlier match`) |
 | `arr.findLast((x) => e)` | — | `SeqFindLast(arr, (x) => e)` (preamble) |
 | `arr.findLastIndex((x) => e)` | — | `SeqFindLastIndex(arr, (x) => e)` (preamble: `-1 ⇔ no match`, `≥0 ⇔ last match with no later match`) |
@@ -622,6 +622,8 @@ Lambda bodies can be expressions (`(x) => x + 1`) or statement blocks (`(x) => {
 
 **filterMap.** `xs.map(x => ... | undefined).filter((x): x is T => x !== undefined)` drops the `undefined`s *and* unwraps to `seq<T>` — lowered to the proven `SeqFilterSome` preamble (a plain `Map(.value, Filter(.Some?, ...))` wouldn't verify, since `.value` is partial).
 
+**`.map` (Dafny).** Lowered to a `seq` comprehension with the element access inlined (`var x := arr[i]; e`), not `Seq.Map`. `Seq.Map` hides the element behind a closure, so a recursive rebuild walker (`Node(kids.map(walk))`) fails Dafny's termination check — the obligation gets quantified over the lambda's parameter instead of anchored at `kids[i]`. Applying a lambda inside the comprehension fails the same way, hence the inlining.
+
 **Monadic callbacks (Lean):** When the callback calls a method, the HOF call uses the monadic variant (e.g., `arr.mapM f`). Pure callbacks use the non-monadic variant (`arr.map f`). The transform checks the transformed lambda body for monadic binds and selects the variant accordingly.
 
 | Pure | Monadic | When |
@@ -647,13 +649,13 @@ The transform uses two strategies for translating `receiver.method(args)`:
 | `s.slice(start, end)` | `stringSlice` | `JSString.slice s start end` | `s[start..end]` |
 | `[...arr, e]` | `arrayPush` | `Array.push arr e` | `(arr + [e])` |
 | `arr.with(i, v)` | `arraySet` | `arr.set! i v` | `arr[i := v]` |
-| `arr.map(f)` | `map` | `arr.map f` | `Std.Collections.Seq.Map(f, arr)` |
+| `arr.map(f)` | `map` | `arr.map f` | seq comprehension (§3.7) |
 | `arr.filter(f)` | `filter` | `arr.filter f` | `Std.Collections.Seq.Filter(f, arr)` |
 | `arr.every(f)` | `every` | `arr.all f` | `Std.Collections.Seq.All(arr, f)` |
 | `arr.some(f)` | `some` | `arr.any f` | `exists x :: x in arr && ...` |
 | `arr.includes(x)` | `includes` | `arr.contains x` | `(x in arr)` |
 | `arr.indexOf(x)` | `indexOf` | — | `SeqIndexOf(arr, x)` |
-| `arr.find(f)` | `find` | `arr.find? f` | — |
+| `arr.find(f)` | `find` | `arr.find? f` | `SeqFind(arr, f)` |
 | `m.get(k)` | `mapGet` | `m.get? k` | `if k in m then Some(m[k]) else None` |
 | `m.has(k)` | `mapHas` | `m.contains k` | `(k in m)` |
 | `m.set(k, v)` | `mapSet` | `m.insert k v` | `m[k := v]` |
diff --git a/SPEC_DAFNY.md b/SPEC_DAFNY.md
index 26a056a..782d10c 100644
--- a/SPEC_DAFNY.md
+++ b/SPEC_DAFNY.md
@@ -92,6 +92,7 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at
 |--------|------|---------|
 | `SeqIndexOf` | `arr.indexOf(x)` | First-index search (`-1` if absent) |
 | `SeqFindIndex` | `arr.findIndex(f)` | Predicate first-index search |
+| `SeqFind` | `arr.find(f)` | Predicate first-match search |
 | `SeqFindLast` | `arr.findLast(f)` | Predicate last-match search |
 | `SeqFilterSome` | filterMap pattern (§3.7) | Drop `None`s and unwrap to `seq<T>` |
 | `SeqFlatten` | `arr.flat()` | Flatten one level |
diff --git a/TOOLS.md b/TOOLS.md
index f2d3861..2bc2ee8 100644
--- a/TOOLS.md
+++ b/TOOLS.md
@@ -59,7 +59,7 @@ Type names: `Expr`, `Stmt`, `Module`, `MatchArm`, `StmtMatchArm`, and `Decl` = `
 
 All TS `receiver.method(args)` calls produce `methodCall` IR nodes carrying the receiver, its type, the TS method name, the args, and a `monadic` flag. No renaming — the IR stores the TS name (`"map"`, `"indexOf"`, `"with"`, `"get"`, etc.) and the receiver type disambiguates.
 
-Each emitter dispatches on `(receiverTy, method)` to decide syntax. For example, `(array, "map")` → Lean: `arr.map f`, Dafny: `Seq.Map(f, arr)`. Unsupported `(type, method)` pairs error at emit time.
+Each emitter dispatches on `(receiverTy, method)` to decide syntax. For example, `(array, "filter")` → Lean: `arr.filter f`, Dafny: `Seq.Filter(f, arr)`. Unsupported `(type, method)` pairs error at emit time.
 
 `app` is reserved for receiver-less calls: user-defined functions, `Pure.fnName(...)`, `JSFloorDiv(a, b)`, `SetToSeq(s)`.
 
diff --git a/examples/arrayFind.def.lean b/examples/arrayFind.def.lean
new file mode 100644
index 0000000..ab88fec
--- /dev/null
+++ b/examples/arrayFind.def.lean
@@ -0,0 +1,16 @@
+/-
+  Generated by lsc from arrayFind.ts
+  Do not edit — re-run `lsc gen` to regenerate.
+-/
+import «arrayFind.types»
+
+set_option loom.semantics.termination "total"
+set_option loom.semantics.choice "demonic"
+
+method lookup (entries : Array Entry) (key : String) return (res : Int)
+  do
+    return Pure.lookup entries key
+
+method hasEntry (entries : Array Entry) (key : String) return (res : Bool)
+  do
+    return Pure.hasEntry entries key
diff --git a/examples/arrayFind.dfy b/examples/arrayFind.dfy
new file mode 100644
index 0000000..8fa05f5
--- /dev/null
+++ b/examples/arrayFind.dfy
@@ -0,0 +1,40 @@
+// Generated by lsc from arrayFind.ts
+
+datatype Option<T> = None | Some(value: T)
+
+function SeqFind<T>(s: seq<T>, p: T -> bool): Option<T>
+  ensures SeqFind(s, p).Some? ==> p(SeqFind(s, p).value)
+  ensures SeqFind(s, p).Some? ==> SeqFind(s, p).value in s
+  ensures SeqFind(s, p).Some? ==>
+    exists i: nat :: i < |s| && s[i] == SeqFind(s, p).value && p(s[i]) &&
+                     (forall j: nat :: j < i ==> !p(s[j]))
+  ensures SeqFind(s, p).None? ==> forall i :: 0 <= i < |s| ==> !p(s[i])
+  decreases |s|
+{
+  if |s| == 0 then None
+  else if p(s[0]) then Some(s[0])
+  else SeqFind(s[1..], p)
+}
+
+datatype Entry = Entry(key: string, val: int)
+
+function lookup(entries: seq<Entry>, key: string): int
+{
+  var e := SeqFind(entries, (x: Entry) => (x.key == key));
+  match (match e { case Some(i_oc0_val) => Option.Some(i_oc0_val.val) case None => Option.None }) {
+    case Some(i_oc1_val) =>
+      i_oc1_val
+    case None =>
+      0
+  }
+}
+
+function hasEntry(entries: seq<Entry>, key: string): bool
+{
+  match SeqFind(entries, (x: Entry) => (x.key == key)) {
+    case Some(i_) =>
+      true
+    case None =>
+      false
+  }
+}
diff --git a/examples/arrayFind.dfy.gen b/examples/arrayFind.dfy.gen
new file mode 100644
index 0000000..8fa05f5
--- /dev/null
+++ b/examples/arrayFind.dfy.gen
@@ -0,0 +1,40 @@
+// Generated by lsc from arrayFind.ts
+
+datatype Option<T> = None | Some(value: T)
+
+function SeqFind<T>(s: seq<T>, p: T -> bool): Option<T>
+  ensures SeqFind(s, p).Some? ==> p(SeqFind(s, p).value)
+  ensures SeqFind(s, p).Some? ==> SeqFind(s, p).value in s
+  ensures SeqFind(s, p).Some? ==>
+    exists i: nat :: i < |s| && s[i] == SeqFind(s, p).value && p(s[i]) &&
+                     (forall j: nat :: j < i ==> !p(s[j]))
+  ensures SeqFind(s, p).None? ==> forall i :: 0 <= i < |s| ==> !p(s[i])
+  decreases |s|
+{
+  if |s| == 0 then None
+  else if p(s[0]) then Some(s[0])
+  else SeqFind(s[1..], p)
+}
+
+datatype Entry = Entry(key: string, val: int)
+
+function lookup(entries: seq<Entry>, key: string): int
+{
+  var e := SeqFind(entries, (x: Entry) => (x.key == key));
+  match (match e { case Some(i_oc0_val) => Option.Some(i_oc0_val.val) case None => Option.None }) {
+    case Some(i_oc1_val) =>
+      i_oc1_val
+    case None =>
+      0
+  }
+}
+
+function hasEntry(entries: seq<Entry>, key: string): bool
+{
+  match SeqFind(entries, (x: Entry) => (x.key == key)) {
+    case Some(i_) =>
+      true
+    case None =>
+      false
+  }
+}
diff --git a/examples/arrayFind.ts b/examples/arrayFind.ts
new file mode 100644
index 0000000..77fd623
--- /dev/null
+++ b/examples/arrayFind.ts
@@ -0,0 +1,21 @@
+/**
+ * `array.find` — first match as an Option (E4).
+ *
+ * `find` returns `T | undefined`, so its result feeds the optional-narrowing
+ * rules: the optChain + nullish on the result exercise `ruleOptChain` /
+ * `ruleNullish` over a `SeqFind` scrutinee. Dafny lowers to the `SeqFind`
+ * preamble helper (first-match ensures); Lean lowers to `.find?`.
+ */
+
+type Entry = { key: string; val: number };
+
+function lookup(entries: Entry[], key: string): number {
+  //@ verify
+  const e = entries.find(x => x.key === key);
+  return e?.val ?? 0;
+}
+
+function hasEntry(entries: Entry[], key: string): boolean {
+  //@ verify
+  return entries.find(x => x.key === key) !== undefined;
+}
diff --git a/examples/arrayFind.types.lean b/examples/arrayFind.types.lean
new file mode 100644
index 0000000..91e3aeb
--- /dev/null
+++ b/examples/arrayFind.types.lean
@@ -0,0 +1,28 @@
+/-
+  Generated by lsc — Lean types and pure function mirrors.
+-/
+import LemmaScript
+
+structure Entry where
+  key : String
+  val : Int
+deriving Repr, Inhabited, DecidableEq
+
+namespace Pure
+
+def lookup (entries : Array Entry) (key : String) : Int :=
+  let e := entries.find? (fun x => x.key = key)
+  match (match e with | .some _oc0_val => Option.some _oc0_val.val | .none => Option.none) with
+  | .some _oc1_val =>
+    _oc1_val
+  | .none =>
+    0
+
+def hasEntry (entries : Array Entry) (key : String) : Bool :=
+  match entries.find? (fun x => x.key = key) with
+  | .some _ =>
+    true
+  | .none =>
+    false
+
+end Pure
diff --git a/examples/ctorName.def.lean b/examples/ctorName.def.lean
new file mode 100644
index 0000000..ef5775d
--- /dev/null
+++ b/examples/ctorName.def.lean
@@ -0,0 +1,21 @@
+/-
+  Generated by lsc from ctorName.ts
+  Do not edit — re-run `lsc gen` to regenerate.
+-/
+import «ctorName.types»
+
+set_option loom.semantics.termination "total"
+set_option loom.semantics.choice "demonic"
+
+method depthOf (k : CallKind) return (res : Int)
+  ensures res ≥ 0
+  do
+    return Pure.depthOf k
+
+method specPure (depth : Int) return (res : CallKind)
+  do
+    return Pure.specPure depth
+
+method plain  return (res : CallKind)
+  do
+    return Pure.plain 
diff --git a/examples/ctorName.dfy b/examples/ctorName.dfy
new file mode 100644
index 0000000..6ffaba2
--- /dev/null
+++ b/examples/ctorName.dfy
@@ -0,0 +1,31 @@
+// Generated by lsc from ctorName.ts
+
+datatype CallKind = spec_pure(depth: int) | plain
+
+function depthOf(k: CallKind): int
+{
+  match k {
+    case spec_pure(i_k_depth) =>
+      if (i_k_depth >= 0) then
+        i_k_depth
+      else
+        0
+    case plain =>
+      0
+  }
+}
+
+lemma depthOf_ensures(k: CallKind)
+  ensures (depthOf(k) >= 0)
+{
+}
+
+function specPure(depth: int): CallKind
+{
+  spec_pure(depth)
+}
+
+function plain(): CallKind
+{
+  CallKind.plain
+}
diff --git a/examples/ctorName.dfy.gen b/examples/ctorName.dfy.gen
new file mode 100644
index 0000000..6ffaba2
--- /dev/null
+++ b/examples/ctorName.dfy.gen
@@ -0,0 +1,31 @@
+// Generated by lsc from ctorName.ts
+
+datatype CallKind = spec_pure(depth: int) | plain
+
+function depthOf(k: CallKind): int
+{
+  match k {
+    case spec_pure(i_k_depth) =>
+      if (i_k_depth >= 0) then
+        i_k_depth
+      else
+        0
+    case plain =>
+      0
+  }
+}
+
+lemma depthOf_ensures(k: CallKind)
+  ensures (depthOf(k) >= 0)
+{
+}
+
+function specPure(depth: int): CallKind
+{
+  spec_pure(depth)
+}
+
+function plain(): CallKind
+{
+  CallKind.plain
+}
diff --git a/examples/ctorName.ts b/examples/ctorName.ts
new file mode 100644
index 0000000..f7d458c
--- /dev/null
+++ b/examples/ctorName.ts
@@ -0,0 +1,36 @@
+/**
+ * Union tags that are not valid identifiers.
+ *
+ * A discriminated union's tag is a source string and may contain characters no
+ * identifier has (`"spec-pure"`). The declaration, the patterns, and the
+ * constructor *applications* must all spell it the same sanitized way —
+ * `spec_pure` in Dafny, `«spec-pure»` in Lean. Applications are the easy one to
+ * miss: they go through a different emit path than declarations and patterns.
+ */
+
+type CallKind =
+  | { kind: "spec-pure"; depth: number }
+  | { kind: "plain" };
+
+export function depthOf(k: CallKind): number {
+  //@ verify
+  //@ ensures \result >= 0
+  switch (k.kind) {
+    case "spec-pure":
+      return k.depth >= 0 ? k.depth : 0;
+    case "plain":
+      return 0;
+  }
+}
+
+// Populated constructor application — the case the sanitizer originally missed.
+export function specPure(depth: number): CallKind {
+  //@ verify
+  return { kind: "spec-pure", depth };
+}
+
+// Nullary constructor application, for contrast.
+export function plain(): CallKind {
+  //@ verify
+  return { kind: "plain" };
+}
diff --git a/examples/ctorName.types.lean b/examples/ctorName.types.lean
new file mode 100644
index 0000000..239a0f4
--- /dev/null
+++ b/examples/ctorName.types.lean
@@ -0,0 +1,29 @@
+/-
+  Generated by lsc — Lean types and pure function mirrors.
+-/
+import LemmaScript
+
+inductive CallKind where
+  | «spec-pure» (depth : Int) : CallKind
+  | plain : CallKind
+deriving Repr, Inhabited
+
+namespace Pure
+
+def depthOf (k : CallKind) : Int :=
+  match k with
+  | .«spec-pure» _k_depth =>
+    if _k_depth ≥ 0 then
+      _k_depth
+    else
+      0
+  | .plain =>
+    0
+
+def specPure (depth : Int) : CallKind :=
+  CallKind.«spec-pure» depth
+
+def plain  : CallKind :=
+  CallKind.plain
+
+end Pure
diff --git a/examples/filterMap.dfy b/examples/filterMap.dfy
index 1312e59..d2a034f 100644
--- a/examples/filterMap.dfy
+++ b/examples/filterMap.dfy
@@ -15,7 +15,7 @@ datatype Out = Out(n: int)
 
 function pick(items: seq<In>): seq<Out>
 {
-  SeqFilterSome(Std.Collections.Seq.Map((it: In) => (if it.keep then Some(Out(it.n)) else None), items))
+  SeqFilterSome(seq(|items|, i_map requires 0 <= i_map < |items| => var it := items[i_map]; (if it.keep then Some(Out(it.n)) else None)))
 }
 
 lemma pick_ensures(items: seq<In>)
diff --git a/examples/filterMap.dfy.gen b/examples/filterMap.dfy.gen
index 1312e59..d2a034f 100644
--- a/examples/filterMap.dfy.gen
+++ b/examples/filterMap.dfy.gen
@@ -15,7 +15,7 @@ datatype Out = Out(n: int)
 
 function pick(items: seq<In>): seq<Out>
 {
-  SeqFilterSome(Std.Collections.Seq.Map((it: In) => (if it.keep then Some(Out(it.n)) else None), items))
+  SeqFilterSome(seq(|items|, i_map requires 0 <= i_map < |items| => var it := items[i_map]; (if it.keep then Some(Out(it.n)) else None)))
 }
 
 lemma pick_ensures(items: seq<In>)
diff --git a/examples/hof.dfy b/examples/hof.dfy
index f4864e7..129f93a 100644
--- a/examples/hof.dfy
+++ b/examples/hof.dfy
@@ -2,7 +2,7 @@
 
 function doubleAll(arr: seq<int>): seq<int>
 {
-  Std.Collections.Seq.Map((x: int) => (x * 2), arr)
+  seq(|arr|, i_map requires 0 <= i_map < |arr| => var x := arr[i_map]; (x * 2))
 }
 
 lemma doubleAll_ensures(arr: seq<int>)
diff --git a/examples/hof.dfy.gen b/examples/hof.dfy.gen
index f4864e7..129f93a 100644
--- a/examples/hof.dfy.gen
+++ b/examples/hof.dfy.gen
@@ -2,7 +2,7 @@
 
 function doubleAll(arr: seq<int>): seq<int>
 {
-  Std.Collections.Seq.Map((x: int) => (x * 2), arr)
+  seq(|arr|, i_map requires 0 <= i_map < |arr| => var x := arr[i_map]; (x * 2))
 }
 
 lemma doubleAll_ensures(arr: seq<int>)
diff --git a/examples/mapRecord.dfy b/examples/mapRecord.dfy
index bbaa6ee..342035a 100644
--- a/examples/mapRecord.dfy
+++ b/examples/mapRecord.dfy
@@ -6,7 +6,7 @@ datatype Out = Out(label_: string, doubled: int)
 
 function relabel(items: seq<In>): seq<Out>
 {
-  Std.Collections.Seq.Map((it: In) => Out(it.tag, (it.n * 2)), items)
+  seq(|items|, i_map requires 0 <= i_map < |items| => var it := items[i_map]; Out(it.tag, (it.n * 2)))
 }
 
 lemma relabel_ensures(items: seq<In>)
diff --git a/examples/mapRecord.dfy.gen b/examples/mapRecord.dfy.gen
index bbaa6ee..342035a 100644
--- a/examples/mapRecord.dfy.gen
+++ b/examples/mapRecord.dfy.gen
@@ -6,7 +6,7 @@ datatype Out = Out(label_: string, doubled: int)
 
 function relabel(items: seq<In>): seq<Out>
 {
-  Std.Collections.Seq.Map((it: In) => Out(it.tag, (it.n * 2)), items)
+  seq(|items|, i_map requires 0 <= i_map < |items| => var it := items[i_map]; Out(it.tag, (it.n * 2)))
 }
 
 lemma relabel_ensures(items: seq<In>)
diff --git a/examples/nullableArray.dfy b/examples/nullableArray.dfy
index 42c21ef..004b62f 100644
--- a/examples/nullableArray.dfy
+++ b/examples/nullableArray.dfy
@@ -16,7 +16,7 @@ function keep(p: Part): bool
 method dropOrphans(messages: seq<Message>) returns (res: seq<Message>)
   ensures (|res| <= |messages|)
 {
-  var filteredContents := Std.Collections.Seq.Map((m: Message) => (match m.content { case ArrayBranch(i_content_arr) => Option.Some(i_content_arr) case _ => Option.None }), messages);
+  var filteredContents := seq(|messages|, i_map requires 0 <= i_map < |messages| => var m := messages[i_map]; (match m.content { case ArrayBranch(i_content_arr) => Option.Some(i_content_arr) case _ => Option.None }));
   var i := 0;
   while (i < |messages|)
     invariant (i <= |messages|)
diff --git a/examples/nullableArray.dfy.gen b/examples/nullableArray.dfy.gen
index 42c21ef..004b62f 100644
--- a/examples/nullableArray.dfy.gen
+++ b/examples/nullableArray.dfy.gen
@@ -16,7 +16,7 @@ function keep(p: Part): bool
 method dropOrphans(messages: seq<Message>) returns (res: seq<Message>)
   ensures (|res| <= |messages|)
 {
-  var filteredContents := Std.Collections.Seq.Map((m: Message) => (match m.content { case ArrayBranch(i_content_arr) => Option.Some(i_content_arr) case _ => Option.None }), messages);
+  var filteredContents := seq(|messages|, i_map requires 0 <= i_map < |messages| => var m := messages[i_map]; (match m.content { case ArrayBranch(i_content_arr) => Option.Some(i_content_arr) case _ => Option.None }));
   var i := 0;
   while (i < |messages|)
     invariant (i <= |messages|)
diff --git a/examples/spec.dfy b/examples/spec.dfy
index 2998e69..888aa7a 100644
--- a/examples/spec.dfy
+++ b/examples/spec.dfy
@@ -200,7 +200,7 @@ function append(arr: seq<int>, x: int): seq<int>
 
 function doubleAll(arr: seq<int>): seq<int>
 {
-  Std.Collections.Seq.Map((x: int) => (x * 2), arr)
+  seq(|arr|, i_map requires 0 <= i_map < |arr| => var x := arr[i_map]; (x * 2))
 }
 
 lemma doubleAll_ensures(arr: seq<int>)
@@ -235,7 +235,7 @@ lemma negate_ensures(x: int)
 
 function negateAll(arr: seq<int>): seq<int>
 {
-  Std.Collections.Seq.Map((x: int) => negate(x), arr)
+  seq(|arr|, i_map requires 0 <= i_map < |arr| => var x := arr[i_map]; negate(x))
 }
 
 lemma negateAll_ensures(arr: seq<int>)
diff --git a/examples/spec.dfy.gen b/examples/spec.dfy.gen
index 2998e69..888aa7a 100644
--- a/examples/spec.dfy.gen
+++ b/examples/spec.dfy.gen
@@ -200,7 +200,7 @@ function append(arr: seq<int>, x: int): seq<int>
 
 function doubleAll(arr: seq<int>): seq<int>
 {
-  Std.Collections.Seq.Map((x: int) => (x * 2), arr)
+  seq(|arr|, i_map requires 0 <= i_map < |arr| => var x := arr[i_map]; (x * 2))
 }
 
 lemma doubleAll_ensures(arr: seq<int>)
@@ -235,7 +235,7 @@ lemma negate_ensures(x: int)
 
 function negateAll(arr: seq<int>): seq<int>
 {
-  Std.Collections.Seq.Map((x: int) => negate(x), arr)
+  seq(|arr|, i_map requires 0 <= i_map < |arr| => var x := arr[i_map]; negate(x))
 }
 
 lemma negateAll_ensures(arr: seq<int>)
diff --git a/examples/switchLambda.dfy b/examples/switchLambda.dfy
index 82761f7..83d1c74 100644
--- a/examples/switchLambda.dfy
+++ b/examples/switchLambda.dfy
@@ -8,7 +8,7 @@ datatype SysMsg = SysMsg(role: string, code: int)
 
 function priorities(msgs: seq<Msg>): seq<int>
 {
-  Std.Collections.Seq.Map((m: Msg) => (match m { case user(i_m_text) => 1 case system(i_m_code) => 2 }), msgs)
+  seq(|msgs|, i_map requires 0 <= i_map < |msgs| => var m := msgs[i_map]; (match m { case user(i_m_text) => 1 case system(i_m_code) => 2 }))
 }
 
 lemma priorities_ensures(msgs: seq<Msg>)
diff --git a/examples/switchLambda.dfy.gen b/examples/switchLambda.dfy.gen
index 82761f7..83d1c74 100644
--- a/examples/switchLambda.dfy.gen
+++ b/examples/switchLambda.dfy.gen
@@ -8,7 +8,7 @@ datatype SysMsg = SysMsg(role: string, code: int)
 
 function priorities(msgs: seq<Msg>): seq<int>
 {
-  Std.Collections.Seq.Map((m: Msg) => (match m { case user(i_m_text) => 1 case system(i_m_code) => 2 }), msgs)
+  seq(|msgs|, i_map requires 0 <= i_map < |msgs| => var m := msgs[i_map]; (match m { case user(i_m_text) => 1 case system(i_m_code) => 2 }))
 }
 
 lemma priorities_ensures(msgs: seq<Msg>)
diff --git a/lakefile.lean b/lakefile.lean
index 4f211db..a16d6e2 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -136,6 +136,8 @@ lean_lib Examples where
     `«postTags.types», `«postTags.def»,
     `«nameClash.types», `«nameClash.def»,
     `«tuples.types», `«tuples.def», `«tuples.proof»,
-    `«forContinue.types», `«forContinue.def», `«forContinue.proof»
+    `«forContinue.types», `«forContinue.def», `«forContinue.proof»,
+    `«arrayFind.types», `«arrayFind.def»,
+    `«ctorName.types», `«ctorName.def»
   ]
   extraDepTargets := #[``downloadDependencies]
diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts
index e471dc8..2a8b168 100644
--- a/tools/src/dafny-emit.ts
+++ b/tools/src/dafny-emit.ts
@@ -3,16 +3,16 @@
  */
 
 import type { Expr, Stmt, Decl, Module, MatchPattern } from "./ir.js";
-import { usesName, usesNameInDecl } from "./ir.js";
+import { usesName, usesNameInDecl, usesNameInStmts } from "./ir.js";
 import type { Ty } from "./typedir.js";
-import { freshName, userNames } from "./names.js";
+import { freshName, freshNameWhere, userNames } from "./names.js";
 import { renameFreeVar } from "./transform.js";
 
 /** Fresh binder for a comprehension wrapping the given subexpressions: `base`
  *  verbatim unless one of them references it, then primed until free. A *local*
  *  check — a same-named name elsewhere in the module keeps the plain binder. */
 function freshBinder(base: string, ...wrapped: Expr[]): string {
-  return freshName(base, name => wrapped.some(w => usesName(w, name)));
+  return freshNameWhere(base, name => wrapped.some(w => usesName(w, name)));
 }
 
 /** Binder + body for lowering a single-return lambda to a comprehension whose
@@ -173,7 +173,7 @@ function methodHeader(prefix: string, params: { name: string; type: Ty }[], retu
   const taken = (n: string): boolean =>
     params.some(p => escapeName(p.name) === n) ||
     (scope !== undefined && usesNameInDecl(scope.requires, scope.ensures, scope.body, n));
-  const resName = freshName("res", taken);
+  const resName = freshNameWhere("res", taken);
   _resultName = resName;
   return `${sig} returns (${resName}: ${tyToDafny(returnType)})`;
 }
@@ -190,9 +190,8 @@ function mapOp(op: string): string { return OP_MAP[op] ?? op; }
 
 // ── Expression emission ─────────────────────────────────────
 
-/** Emit a match scrutinee — either a variable name (string) or an expression. */
-function emitScrutinee(s: string | Expr): string {
-  return typeof s === "string" ? escapeName(s) : emitExpr(s);
+function emitScrutinee(s: Expr): string {
+  return emitExpr(s);
 }
 
 /** Collapse nested forall/exists into a single quantifier with multiple bound vars. */
@@ -280,11 +279,51 @@ function emitExpr(e: Expr): string {
           }
           return `${obj}[${args[0]}..${args[1]}]`;
         }
-        if (e.method === "map")    return `Std.Collections.Seq.Map(${args[0]}, ${obj})`;
+        if (e.method === "map") {
+          // Always a seq comprehension: Seq.Map would hide the element access
+          // behind a closure, defeating Dafny's termination checker for
+          // recursive rebuild walkers. A literal lambda argument is
+          // beta-reduced through a `var` binding — an applied closure defeats
+          // the checker too; any other argument is applied to the element
+          // directly. A non-variable receiver is bound once up front: the
+          // comprehension mentions it three times, and splicing would make
+          // any closure literal inside it (e.g. a Filter predicate) three
+          // distinct closures, unprovably equal through an opaque callee.
+          // Name freshness is a local IR-level check until a backend name
+          // allocator exists.
+          const lam = e.args[0];
+          const fresh = (base: string, taken: (n: string) => boolean): string => {
+            let name = base;
+            for (let n = 2; taken(name); n++) name = `${base}${n}`;
+            return name;
+          };
+          const taken = (n: string): boolean =>
+            usesName(e.obj, n) || usesName(lam, n) ||
+            (lam.kind === "lambda" && (lam.params.some(pp => pp.name === n) ||
+              usesNameInStmts(lam.body, n)));
+          const bind = e.obj.kind !== "var";
+          const s = bind ? fresh("s_map", taken) : obj;
+          const idx = fresh("i_map", n => taken(n) || n === s);
+          let core: string;
+          if (lam.kind === "lambda" && lam.params.length === 1 &&
+              lam.body.length === 1 && lam.body[0].kind === "return") {
+            const p = escapeName(lam.params[0].name);
+            core = `var ${p} := ${s}[${idx}]; ${emitExpr(lam.body[0].value)}`;
+          } else {
+            core = `(${args[0]})(${s}[${idx}])`;
+          }
+          const comp = `seq(|${s}|, ${idx} requires 0 <= ${idx} < |${s}| => ${core})`;
+          return bind ? `(var ${s} := ${obj}; ${comp})` : comp;
+        }
         if (e.method === "filter") return `Std.Collections.Seq.Filter(${args[0]}, ${obj})`;
         // filterMap (synthesized in resolve): drop Nones and unwrap to seq<T>.
         if (e.method === "filterSome") { needPreamble("SeqFilterSome"); needPreamble("OptionType"); return `SeqFilterSome(${obj})`; }
         if (e.method === "every")  return `Std.Collections.Seq.All(${obj}, ${args[0]})`;
+        if (e.method === "find") {
+          needPreamble("OptionType");
+          needPreamble("SeqFind");
+          return `SeqFind(${obj}, ${args[0]})`;
+        }
         if (e.method === "findLast") {
           needPreamble("OptionType");
           needPreamble("SeqFindLast");
@@ -491,6 +530,15 @@ function emitExpr(e: Expr): string {
       if (e.fn === "MinOfSeq") { needPreamble("MathMin"); needPreamble("MinOfSeq"); }
       if (e.fn === "Perm") needPreamble("Perm");
       if (e.fn === "SetFromSeq") needPreamble("SetFromSeq");
+      // A constructor application must spell the name the same way the
+      // datatype declaration does — `dafnyCtorName`, not `escapeName`, since
+      // tags come from source strings ("spec-pure") that escapeName leaves alone.
+      if (e.ctorOf) {
+        const ctor = dafnyCtorName(e.fn);
+        return _ambiguousCtors.has(e.fn)
+          ? `${e.ctorOf}.${ctor}(${args.join(", ")})`
+          : `${ctor}(${args.join(", ")})`;
+      }
       return `${escapeName(e.fn)}(${args.join(", ")})`;
     }
 
@@ -501,6 +549,10 @@ function emitExpr(e: Expr): string {
       if (!e.datatypeField && (e.field === "size" || e.field === "length" || e.field === "collectionSize")) return `|${obj}|`;
       if (!e.datatypeField && e.field === "keys") return `${obj}.Keys`;
       if (e.field === "toNat") return obj;
+      if (e.ctor && e.fromUnion) {
+        const renamed = _ctorFieldRenames.get(`${e.fromUnion}.${e.ctor}.${e.field}`);
+        if (renamed) return `${obj}.${escapeName(renamed)}`;
+      }
       return `${obj}.${escapeName(e.field)}`;
     }
 
@@ -525,7 +577,10 @@ function emitExpr(e: Expr): string {
         if (e.fields.length === 0) {
           return emitExpr(e.spread);
         }
-        const updates = e.fields.map(f => `${escapeName(f.name)} := ${emitExpr(f.value)}`);
+        const updates = e.fields.map(f => {
+          const renamed = e.ctor && e.ctorOf ? _ctorFieldRenames.get(`${e.ctorOf}.${e.ctor}.${f.name}`) : undefined;
+          return `${escapeName(renamed ?? f.name)} := ${emitExpr(f.value)}`;
+        });
         return `${emitExpr(e.spread)}.(${updates.join(", ")})`;
       }
       // Match constructor by field names — prefer exact match over first-field heuristic
@@ -726,9 +781,9 @@ function emitDecl(d: Decl): string {
         }
       const collides = new Set([...typesByField].filter(([, s]) => s.size > 1).map(([n]) => n));
       const ctors = d.constructors.map(c => {
-        if (c.fields.length === 0) return escapeName(c.name);
-        const fields = c.fields.map(f => collides.has(f.name) ? { ...f, name: `${f.name}_${c.name}` } : f);
-        return `${escapeName(c.name)}(${paramList(fields)})`;
+        if (c.fields.length === 0) return dafnyCtorName(c.name);
+        const fields = c.fields.map(f => collides.has(f.name) ? { ...f, name: `${f.name}_${c.name.replace(/[^A-Za-z0-9_'?]/g, "_")}` } : f);
+        return `${dafnyCtorName(c.name)}(${paramList(fields)})`;
       });
       return `datatype ${escapeName(d.name)}${tp} = ${ctors.join(" | ")}`;
     }
@@ -984,6 +1039,20 @@ const SEQ_FIND_LAST_INDEX = `function SeqFindLastIndex<T>(s: seq<T>, p: T -> boo
   else SeqFindLastIndex(s[..|s|-1], p)
 }`;
 
+const SEQ_FIND = `function SeqFind<T>(s: seq<T>, p: T -> bool): Option<T>
+  ensures SeqFind(s, p).Some? ==> p(SeqFind(s, p).value)
+  ensures SeqFind(s, p).Some? ==> SeqFind(s, p).value in s
+  ensures SeqFind(s, p).Some? ==>
+    exists i: nat :: i < |s| && s[i] == SeqFind(s, p).value && p(s[i]) &&
+                     (forall j: nat :: j < i ==> !p(s[j]))
+  ensures SeqFind(s, p).None? ==> forall i :: 0 <= i < |s| ==> !p(s[i])
+  decreases |s|
+{
+  if |s| == 0 then None
+  else if p(s[0]) then Some(s[0])
+  else SeqFind(s[1..], p)
+}`;
+
 const SEQ_FIND_LAST = `function SeqFindLast<T>(s: seq<T>, p: T -> bool): Option<T>
   ensures SeqFindLast(s, p).Some? ==> p(SeqFindLast(s, p).value)
   ensures SeqFindLast(s, p).Some? ==> SeqFindLast(s, p).value in s
@@ -1262,6 +1331,7 @@ const PREAMBLE_CODE: [string, string][] = [
   ["SeqFindIndex", SEQ_FIND_INDEX],
   ["SeqFindLastIndex", SEQ_FIND_LAST_INDEX],
   ["SeqFilterSome", SEQ_FILTER_SOME],
+  ["SeqFind", SEQ_FIND],
   ["SeqFindLast", SEQ_FIND_LAST],
   ["SeqFlatten", SEQ_FLATTEN],
   ["SeqJoin", SEQ_JOIN],
@@ -1289,18 +1359,51 @@ const PREAMBLE_CODE: [string, string][] = [
 let _recordCtors = new Map<string, string>();
 let _structureDecls = new Map<string, { name: string; type: Ty }[]>();
 let _declaredTypes = new Set<string>();
+let _ambiguousCtors = new Set<string>();
+// `"<union>.<ctor>.<field>"` → per-constructor destructor name, for fields the
+// inductive emission renames (shared name, differing types). Field reads and
+// datatype updates with a pinned ctor must use the renamed destructor.
+let _ctorFieldRenames = new Map<string, string>();
 
 function buildRecordCtorMap(decls: Decl[]) {
   _recordCtors = new Map();
   _structureDecls = new Map();
   _declaredTypes = new Set();
+  _ambiguousCtors = new Set();
+  _ctorFieldRenames = new Map();
+  const ctorSeen = new Set<string>();
   function collectDecl(d: Decl) {
     if (d.kind === "structure") {
       _declaredTypes.add(d.name);
       _structureDecls.set(d.name, d.fields);
       if (d.fields.length > 0) _recordCtors.set(d.fields[0].name, d.name);
     }
-    if (d.kind === "inductive") _declaredTypes.add(d.name);
+    if (d.kind === "inductive") {
+      _declaredTypes.add(d.name);
+      // Constructor names shared by two datatypes in this module (Expr.let vs
+      // Stmt.let) can't be used bare — emitters must qualify them.
+      for (const c of d.constructors) {
+        if (ctorSeen.has(c.name)) _ambiguousCtors.add(c.name);
+        ctorSeen.add(c.name);
+      }
+      // Mirror the destructor renaming the inductive case of emitDecl performs
+      // (shared field name, differing types → per-constructor names), so reads
+      // and updates can be translated to the renamed destructors.
+      const typesByField = new Map<string, Set<string>>();
+      for (const c of d.constructors)
+        for (const f of c.fields) {
+          let s = typesByField.get(f.name);
+          if (!s) { s = new Set(); typesByField.set(f.name, s); }
+          s.add(tyToDafny(f.type));
+        }
+      const collides = new Set([...typesByField].filter(([, s]) => s.size > 1).map(([n]) => n));
+      for (const c of d.constructors)
+        for (const f of c.fields) {
+          if (!collides.has(f.name)) continue;
+          _ctorFieldRenames.set(`${d.name}.${c.name}.${f.name}`,
+            `${f.name}_${c.name.replace(/[^A-Za-z0-9_'?]/g, "_")}`);
+        }
+    }
     if (d.kind === "type-alias") _declaredTypes.add(d.name);
     if (d.kind === "def") _declaredTypes.add(d.name);
     if (d.kind === "namespace") for (const inner of d.decls) collectDecl(inner);
@@ -1319,9 +1422,20 @@ function resolveTy(ty: Ty): Ty {
   return ty;
 }
 
+/** Constructor names come from source strings (string-union values like
+ *  "spec-pure", discriminated-union tags), which may contain characters no
+ *  TS identifier has; map those to `_` before the ordinary escaping. A
+ *  collision after mapping fails loudly in Dafny (duplicate constructor)
+ *  rather than silently merging. */
+function dafnyCtorName(name: string): string {
+  return escapeName(name.replace(/[^A-Za-z0-9_'?]/g, "_"));
+}
+
 function qualifyCtor(name: string, type?: string): string {
   const rawName = name.replace(/^\./, "");
-  const mapped = CTOR_MAP[rawName] ?? escapeName(rawName);
+  // hasOwn: a ctor literally named "constructor" (the IR's own Expr variant)
+  // must not hit Object.prototype.constructor through the bare index.
+  const mapped = (Object.hasOwn(CTOR_MAP, rawName) ? CTOR_MAP[rawName] : undefined) ?? dafnyCtorName(rawName);
   if (type) return `${type}.${mapped}`;
   return mapped;
 }
@@ -1335,7 +1449,7 @@ const CTOR_MAP: Record<string, string> = { "some": "Some", "none": "None" };
 
 function translatePattern(p: MatchPattern): string {
   if (p.kind === "wild") return "_";
-  const ctorName = CTOR_MAP[p.ctor] ?? escapeName(p.ctor);
+  const ctorName = (Object.hasOwn(CTOR_MAP, p.ctor) ? CTOR_MAP[p.ctor] : undefined) ?? dafnyCtorName(p.ctor);
   if (p.binders.length === 0) return ctorName;
   return `${ctorName}(${p.binders.map(escapeName).join(", ")})`;
 }
diff --git a/tools/src/extract.ts b/tools/src/extract.ts
index 7419eba..73d7e7d 100644
--- a/tools/src/extract.ts
+++ b/tools/src/extract.ts
@@ -21,6 +21,14 @@ let _havocKey: string | null = null;
  *  different `.ts` source file. Emitted in Dafny as `function {:axiom} <flat>`.
  *  Cleared at the start of every `extractModule`. */
 const _externs = new Map<string, import("./rawir.js").RawExtern>();
+/** Signature types of *kept* externs, for the imported-type resolver: a type
+ *  reachable ONLY through an imported function's signature (e.g. an extern
+ *  returning PresentFact that no local signature mentions) must still be
+ *  resolved into a full decl, or it synthesizes opaque. Filled only after the
+ *  extern survives the `_externs` dedup — a cross-file signature superseded by a
+ *  same-file `//@ extern` contributes nothing to the output, so resolving its
+ *  types would emit decls that no emitted declaration mentions. */
+const _externSigTypes: { type: Type; node: Node }[] = [];
 let _currentSourceFile: SourceFile | null = null;
 /** True only while extracting a function body. Module-level constants that
  *  reference cross-file callees (e.g., `BusEvent.define(...)` inside a
@@ -40,9 +48,13 @@ function registerExternIfCrossFile(
   callee: import("ts-morph").PropertyAccessExpression | import("ts-morph").Identifier,
   sourceFile: SourceFile,
 ): void {
-  const ext = detectCrossFileExtern(callee, sourceFile);
+  const sigTypes: { type: Type; node: Node }[] = [];
+  const ext = detectCrossFileExtern(callee, sourceFile, sigTypes);
   if (!ext || _externs.has(ext.qualified)) return;
   _externs.set(ext.qualified, ext);
+  // Only now that the extern is kept do its signature types become resolver
+  // seeds — see `_externSigTypes`.
+  _externSigTypes.push(...sigTypes);
   // Recurse: scan the source decl's body for nested cross-file calls so any
   // symbol referenced by the copied spec is itself declared in the output.
   let symbol = callee.getSymbol();
@@ -67,6 +79,7 @@ function registerExternIfCrossFile(
 function detectCrossFileExtern(
   callee: import("ts-morph").PropertyAccessExpression | import("ts-morph").Identifier,
   sourceFile: SourceFile,
+  sigTypesOut: { type: Type; node: Node }[],
 ): import("./rawir.js").RawExtern | null {
   let symbol = callee.getSymbol();
   if (!symbol) return null;
@@ -96,13 +109,31 @@ function detectCrossFileExtern(
   // kept): a bare `TMsg`, not `import("/abs/path/transcript").TMsg` — the
   // importing module declares the datatype locally, so the axiom must use the
   // local name.
+  // NoTruncation: a wide expansion (e.g. an alias for a large string-literal
+  // union, not importable at the call site) must print whole — a truncated
+  // union is unparseable and synthesizes an opaque decl named by its own text.
   const externTypeText = (t: Type) =>
-    t.getText(callee, ts.TypeFormatFlags.UseAliasDefinedOutsideCurrentScope);
+    t.getText(callee, ts.TypeFormatFlags.UseAliasDefinedOutsideCurrentScope | ts.TypeFormatFlags.NoTruncation);
   const params = sig.getParameters().map(p => ({
     name: p.getName(),
     tsType: externTypeText(p.getTypeAtLocation(callee)),
   }));
   const returnType = externTypeText(sig.getReturnType());
+  for (const p of sig.getParameters()) {
+    sigTypesOut.push({ type: p.getTypeAtLocation(callee), node: callee });
+  }
+  sigTypesOut.push({ type: sig.getReturnType(), node: callee });
+  // Also seed from the source declaration's syntactic type nodes: symbol-based
+  // types can drop the alias symbol (the printed signature then names an alias
+  // like `TypeDecls` that would otherwise synthesize opaque), while a type
+  // node's type keeps it.
+  const srcDecl = externalDecl as { getParameters?: () => { getTypeNode?: () => Node | undefined }[]; getReturnTypeNode?: () => Node | undefined };
+  for (const sp of srcDecl.getParameters?.() ?? []) {
+    const tn = sp.getTypeNode?.();
+    if (tn) sigTypesOut.push({ type: tn.getType(), node: tn });
+  }
+  const rtn = srcDecl.getReturnTypeNode?.();
+  if (rtn) sigTypesOut.push({ type: rtn.getType(), node: rtn });
   let qualified: string;
   if (Node.isPropertyAccessExpression(callee)) {
     qualified = `${callee.getExpression().getText()}.${callee.getName()}`;
@@ -470,10 +501,9 @@ function extractExpr(node: Expression): RawExpr {
       const typeNode = p.getTypeNode();
       return { name: p.getName(), tsType: typeNode ? typeNode.getText() : undefined };
     });
-    // Capture an explicit return annotation (`(x): Out => …`) so resolve can type
-    // return-position record literals to their named type instead of a tuple.
-    const retNode = node.getReturnTypeNode();
-    const returnTsType = retNode ? typeToString(node.getReturnType()) : undefined;
+    // Return type from the checker — inferred when unannotated — so resolve can
+    // type return-position record literals and give the lambda a real fn type.
+    const returnTsType = typeToString(node.getReturnType());
     const body = node.getBody();
     if (Node.isExpression(body)) {
       return { kind: "lambda", params, body: extractExpr(body), returnTsType };
@@ -707,8 +737,12 @@ function extractTypeDecl(decl: TypeAliasDeclaration, extraDecls?: TypeDeclInfo[]
             if (prop.getName() === discriminant) continue;
             let tsType = typeToString(prop.getTypeAtLocation(decl));
             const propDecl = prop.getDeclarations()[0];
-            if (propDecl && (propDecl as any).hasQuestionToken?.() && !tsType.includes(" | undefined")) {
-              tsType = `${tsType} | undefined`;
+            tsType = declaredTypeTextIfBetter(propDecl, tsType);
+            if (propDecl && (propDecl as any).hasQuestionToken?.()) {
+              // Normalize checker output that puts `undefined` first, then
+              // ensure exactly one trailing `| undefined`.
+              if (tsType.startsWith("undefined | ")) tsType = `${tsType.slice("undefined | ".length)} | undefined`;
+              else if (!tsType.includes(" | undefined")) tsType = `${tsType} | undefined`;
             }
             fields.push({ name: prop.getName(), tsType });
           }
@@ -796,12 +830,16 @@ function extractRecord(name: string, type: Type, locationNode: Node, overrides?:
 
     const propType = prop.getTypeAtLocation(locationNode);
     let tsType = typeToString(propType);
+    const propDecl = prop.getDeclarations()[0];
+    tsType = declaredTypeTextIfBetter(propDecl, tsType);
     // Optional property: `foo?: T` reports as `T` (ts-morph strips the
     // `| undefined` from a question-token type). Add it back so the field
     // resolves to `Optional<T>`.
-    const propDecl = prop.getDeclarations()[0];
-    if (propDecl && (propDecl as any).hasQuestionToken?.() && !tsType.includes(" | undefined")) {
-      tsType = `${tsType} | undefined`;
+    if (propDecl && (propDecl as any).hasQuestionToken?.()) {
+      // Normalize checker output that puts `undefined` first, then ensure
+      // exactly one trailing `| undefined`.
+      if (tsType.startsWith("undefined | ")) tsType = `${tsType.slice("undefined | ".length)} | undefined`;
+      else if (!tsType.includes(" | undefined")) tsType = `${tsType} | undefined`;
     }
 
     // Inline anonymous object types: ts-morph names them __type.
@@ -849,6 +887,21 @@ function findDiscriminant(members: Type[]): string | null {
   return null;
 }
 
+/** Recover a field's *declared* type text when the semantic printer degraded
+ *  to ts-morph's anonymous `__type` — a self-referential alias reached
+ *  through a `| null` union expands structurally and loses its name. The
+ *  syntactic node text preserves the alias spelling (`TExpr | null`). Only
+ *  plain reference text is used: inline object literals (containing `{`)
+ *  keep the `__type` marker so record synthesis can handle them. */
+function declaredTypeTextIfBetter(propDecl: Node | undefined, tsType: string): string {
+  if (!tsType.includes("__type") || !propDecl) return tsType;
+  const tn = (propDecl as { getTypeNode?: () => Node | undefined }).getTypeNode?.();
+  if (!tn) return tsType;
+  const text = tn.getText();
+  if (text.includes("__type") || text.includes("{")) return tsType;
+  return text;
+}
+
 function typeToString(type: Type): string {
   if (type.isUndefined()) return "undefined";
   if (type.isNumber() || type.isNumberLiteral()) return "number";
@@ -1860,6 +1913,7 @@ export function extractModule(sourceFile: SourceFile): RawModule {
   // `extractExpr` during call extraction (only symbols *actually used* end up
   // here), deduped by qualified name.
   _externs.clear();
+  _externSigTypes.length = 0;
 
   // Share the module's ts-morph Project with parseTsType (scratch source file
   // for type-string parsing). Done before declare-type parsing so any
@@ -2307,10 +2361,12 @@ export function extractModule(sourceFile: SourceFile): RawModule {
   // Resolve imported types: extract types referenced in function signatures but not in this file
   const knownTypes = new Set(typeDecls.map(d => d.name));
   const builtins = new Set(["Map", "Set", "Array", "String", "Number", "Boolean", "Promise", "Date", "RegExp", "Error"]);
+  const visitedTypes = new Set<unknown>();
   function resolveType(t: Type, locationNode: Node) {
-    // Unwrap arrays and generics to find user-defined types
-    if (t.isArray()) { resolveType(t.getArrayElementTypeOrThrow(), locationNode); return; }
-    // Resolve type aliases (e.g. string unions imported from other files)
+    // Resolve type aliases (e.g. string unions imported from other files).
+    // BEFORE the visited guard: the same interned compilerType can arrive both
+    // with and without its alias symbol (getTypeAtLocation drops it), and an
+    // aliasless first visit must not suppress the alias extraction.
     const alias = t.getAliasSymbol();
     if (alias) {
       const aliasName = alias.getName();
@@ -2333,6 +2389,14 @@ export function extractModule(sourceFile: SourceFile): RawModule {
         }
       }
     }
+    // Recursion guard: recursive unions (Expr → variant → body: Expr) are
+    // reachable now that anonymous variant fields are walked below. Keyed on
+    // the compiler's interned Type object — alias names are not enough,
+    // because getTypeAtLocation can drop the alias symbol.
+    if (visitedTypes.has(t.compilerType)) return;
+    visitedTypes.add(t.compilerType);
+    // Unwrap arrays and generics to find user-defined types
+    if (t.isArray()) { resolveType(t.getArrayElementTypeOrThrow(), locationNode); return; }
     if (t.isUnion()) { for (const u of t.getUnionTypes()) resolveType(u, locationNode); return; }
     for (const arg of t.getTypeArguments()) resolveType(arg, locationNode);
     const sym = t.getSymbol() ?? t.getAliasSymbol();
@@ -2347,6 +2411,14 @@ export function extractModule(sourceFile: SourceFile): RawModule {
           resolveType(prop.getTypeAtLocation(locationNode), locationNode);
         }
       }
+    } else if (t.isObject() && (!name || name.startsWith("__")) && t.getCallSignatures().length === 0) {
+      // Anonymous object type — typically a variant of an imported
+      // discriminated union. There is no decl to extract, but its fields can
+      // reference named types (`arms: MatchArm[]`) that downstream passes
+      // need declared, so walk them.
+      for (const prop of t.getProperties()) {
+        resolveType(prop.getTypeAtLocation(locationNode), locationNode);
+      }
     }
   }
   for (let i = 0; i < fnsToExtract.length; i++) {
@@ -2362,6 +2434,8 @@ export function extractModule(sourceFile: SourceFile): RawModule {
       resolveType(p.getType(), p);
     }
   }
+  // Extern signature types: see _externSigTypes.
+  for (const r of _externSigTypes) resolveType(r.type, r.node);
   // Resolve anonymous object return types into synthetic named types
   for (let i = 0; i < fnsToExtract.length; i++) {
     const f = fnsToExtract[i];
diff --git a/tools/src/ir.ts b/tools/src/ir.ts
index f06f0d1..15a7fbd 100644
--- a/tools/src/ir.ts
+++ b/tools/src/ir.ts
@@ -14,7 +14,7 @@ export type Expr =
   | { kind: "num"; value: number }
   | { kind: "bool"; value: boolean }
   | { kind: "str"; value: string }
-  | { kind: "constructor"; name: string; type?: string; args?: Expr[] }   // .idle / .some x — name is lowercase; emitters capitalize per backend
+  | { kind: "constructor"; name: string; type?: string; args: Expr[] }   // .idle / .some x — name is lowercase; emitters capitalize per backend
   | { kind: "binop"; op: string; left: Expr; right: Expr }
   | { kind: "unop"; op: string; expr: Expr }
   | { kind: "app"; fn: string; args: Expr[]; ctorOf?: string }  // f a b; ctorOf set ⇒ fn is a datatype constructor of that (base) type. Dafny takes the bare name `fn(args)`; Lean must qualify it as `ctorOf.fn args`.
@@ -24,15 +24,15 @@ export type Expr =
   | { kind: "index"; arr: Expr; idx: Expr }                // arr[idx]!
   | { kind: "tupleLiteral"; elems: Expr[] }                // (a, b) — heterogeneous tuple literal
   | { kind: "tupleProj"; obj: Expr; index: number; arity: number }  // projection at a 0-based position; arity is needed only by Lean, whose right-nested Prod makes the last slot asymmetric (Dafny just uses `t.index`)
-  | { kind: "record"; spread: Expr | null; fields: { name: string; value: Expr }[]; ctor?: string }
+  | { kind: "record"; spread: Expr | null; fields: RecordField[]; ctor?: string; ctorOf?: string }  // ctorOf: the union whose variant `ctor` is, when a datatype update needs renamed destructors
   | { kind: "arrayLiteral"; elems: Expr[] }
   | { kind: "emptyMap" }
   | { kind: "emptySet" }
-  | { kind: "mapLiteral"; entries: { key: Expr; value: Expr }[] }
+  | { kind: "mapLiteral"; entries: MapEntry[] }
   | { kind: "methodCall"; obj: Expr; objTy: Ty; method: string; args: Expr[]; monadic: boolean }
-  | { kind: "lambda"; params: { name: string; type: Ty }[]; body: Stmt[] }
+  | { kind: "lambda"; params: Param[]; body: Stmt[] }
   | { kind: "if"; cond: Expr; then: Expr; else: Expr }
-  | { kind: "match"; scrutinee: string | Expr; arms: MatchArm[] }
+  | { kind: "match"; scrutinee: Expr; arms: MatchArm[] }
   | { kind: "forall"; var: string; type: Ty; body: Expr }
   | { kind: "exists"; var: string; type: Ty; body: Expr }
   | { kind: "implies"; premises: Expr[]; conclusion: Expr }
@@ -48,7 +48,16 @@ export type MatchPattern =
   | { kind: "ctor"; ctor: string; binders: string[] };  // ".some x" ⇒ {ctor:"some", binders:["x"]}; ".none" ⇒ binders:[]
 
 export const pWild = (): MatchPattern => ({ kind: "wild" });
-export const pCtor = (ctor: string, ...binders: string[]): MatchPattern => ({ kind: "ctor", ctor, binders });
+export const pCtor = (c: string, ...binders: string[]): MatchPattern => ({ kind: "ctor", ctor: c, binders });
+
+// Named payload records for the shapes repeated across IR nodes. Purely
+// structural — identical to the object-literal types they replace, so
+// construction sites are unaffected.
+export interface Param { name: string; type: Ty }
+export interface RecordField { name: string; value: Expr }
+export interface MapEntry { key: Expr; value: Expr }
+export interface CtorInfo { name: string; fields: Param[] }
+export interface EmitOption { key: string; value: string }
 
 /** Binder identifiers a pattern introduces (`[]` for wildcard / nullary ctor). */
 export function patternBinders(p: MatchPattern): string[] {
@@ -78,7 +87,7 @@ export type Stmt =
   | { kind: "break" }
   | { kind: "continue" }
   | { kind: "if"; cond: Expr; then: Stmt[]; else: Stmt[] }
-  | { kind: "match"; scrutinee: string | Expr; arms: StmtMatchArm[] }
+  | { kind: "match"; scrutinee: Expr; arms: StmtMatchArm[] }
   | { kind: "while"; cond: Expr; invariants: Expr[]; decreasing: Expr | null;
       doneWith: Expr | null; body: Stmt[] }
   | { kind: "forin"; idx: string; bound: Expr; invariants: Expr[]; body: Stmt[] }
@@ -97,7 +106,7 @@ export interface Inductive {
   kind: "inductive";
   name: string;
   typeParams?: string[];
-  constructors: { name: string; fields: { name: string; type: Ty }[] }[];
+  constructors: CtorInfo[];
   deriving: string[];
 }
 
@@ -105,7 +114,7 @@ export interface Structure {
   kind: "structure";
   name: string;
   typeParams?: string[];
-  fields: { name: string; type: Ty }[];
+  fields: Param[];
   deriving: string[];
 }
 
@@ -113,7 +122,7 @@ export interface FnDef {
   kind: "def";
   name: string;
   typeParams: string[];
-  params: { name: string; type: Ty }[];
+  params: Param[];
   returnType: Ty;
   requires: Expr[];  // used by Dafny backend; Lean backend ignores
   ensures: Expr[];   // used by Dafny backend for companion lemma
@@ -125,7 +134,7 @@ export interface FnDefByMethod {
   kind: "def-by-method";
   name: string;
   typeParams: string[];
-  params: { name: string; type: Ty }[];
+  params: Param[];
   returnType: Ty;
   requires: Expr[];
   ensures: Expr[];
@@ -137,7 +146,7 @@ export interface FnMethod {
   kind: "method";
   name: string;
   typeParams: string[];
-  params: { name: string; type: Ty }[];
+  params: Param[];
   returnType: Ty;
   requires: Expr[];
   ensures: Expr[];
@@ -154,7 +163,7 @@ export interface Namespace {
 export interface ClassDecl {
   kind: "class";
   name: string;
-  fields: { name: string; type: Ty }[];
+  fields: Param[];
   methods: FnMethod[];
 }
 
@@ -190,7 +199,7 @@ export interface ExternDecl {
   kind: "extern";
   name: string;                                 // flat name (dots → underscores)
   typeParams: string[];                         // generic type parameters (e.g. ["S", "A"])
-  params: { name: string; type: Ty }[];
+  params: Param[];
   returnType: Ty;
   requires: Expr[];
   ensures: Expr[];
@@ -201,7 +210,7 @@ export type Decl = Inductive | Structure | FnDef | FnDefByMethod | FnMethod | Na
 export interface Module {
   comment: string;
   imports: string[];
-  options: { key: string; value: string }[];
+  options: EmitOption[];
   decls: Decl[];
 }
 
@@ -221,7 +230,7 @@ export function anyExpr(e: Expr, pred: ExprPred): boolean {
   switch (e.kind) {
     case "var": case "num": case "bool": case "str":
     case "emptyMap": case "emptySet": case "havoc": case "default": return false;
-    case "constructor": return (e.args ?? []).some(a => anyExpr(a, pred));
+    case "constructor": return e.args.some(a => anyExpr(a, pred));
     case "binop": return anyExpr(e.left, pred) || anyExpr(e.right, pred);
     case "unop": case "toNat": case "toReal": return anyExpr(e.expr, pred);
     case "app": return e.args.some(a => anyExpr(a, pred));
@@ -236,7 +245,7 @@ export function anyExpr(e: Expr, pred: ExprPred): boolean {
     case "methodCall": return anyExpr(e.obj, pred) || e.args.some(a => anyExpr(a, pred));
     case "lambda": return e.body.some(s => anyExprInStmt(s, pred));
     case "if": return anyExpr(e.cond, pred) || anyExpr(e.then, pred) || anyExpr(e.else, pred);
-    case "match": return (typeof e.scrutinee !== "string" && anyExpr(e.scrutinee, pred)) || e.arms.some(a => anyExpr(a.body, pred));
+    case "match": return anyExpr(e.scrutinee, pred) || e.arms.some(a => anyExpr(a.body, pred));
     case "forall": case "exists": return anyExpr(e.body, pred);
     case "let": return anyExpr(e.value, pred) || anyExpr(e.body, pred);
   }
@@ -249,7 +258,7 @@ export function anyExprInStmt(s: Stmt, pred: ExprPred): boolean {
     case "assert": return anyExpr(s.expr, pred);
     case "break": case "continue": return false;
     case "if": return anyExpr(s.cond, pred) || anyExprInStmts(s.then, pred) || anyExprInStmts(s.else, pred);
-    case "match": return (typeof s.scrutinee !== "string" && anyExpr(s.scrutinee, pred)) || s.arms.some(a => anyExprInStmts(a.body, pred));
+    case "match": return anyExpr(s.scrutinee, pred) || s.arms.some(a => anyExprInStmts(a.body, pred));
     case "while": return anyExpr(s.cond, pred) || s.invariants.some(i => anyExpr(i, pred))
       || (s.decreasing ? anyExpr(s.decreasing, pred) : false) || (s.doneWith ? anyExpr(s.doneWith, pred) : false)
       || anyExprInStmts(s.body, pred);
@@ -267,10 +276,9 @@ export function anyExprInStmts(stmts: Stmt[], pred: ExprPred): boolean {
 // (the result out-parameter, comprehension binders): a binder is checked only
 // against the expressions/scope it actually wraps, not the whole module.
 const _refsName = (name: string): ExprPred =>
-  e => (e.kind === "var" && e.name === name) ||
+  (e: Expr) => (e.kind === "var" && e.name === name) ||
        (e.kind === "app" && e.fn === name) ||
-       (e.kind === "constructor" && e.name === name) ||
-       (e.kind === "match" && typeof e.scrutinee === "string" && e.scrutinee === name);
+       (e.kind === "constructor" && e.name === name);
 
 export function usesName(e: Expr, name: string): boolean {
   return anyExpr(e, _refsName(name));
diff --git a/tools/src/lean-emit.ts b/tools/src/lean-emit.ts
index 8ae4bf6..eedc13d 100644
--- a/tools/src/lean-emit.ts
+++ b/tools/src/lean-emit.ts
@@ -8,7 +8,7 @@
 import type { Expr, Stmt, Decl, Module, MatchPattern } from "./ir.js";
 import { anyExpr, usesNameInDecl, patternBinders } from "./ir.js";
 import type { Ty } from "./typedir.js";
-import { freshName } from "./names.js";
+import { freshName, freshNameWhere } from "./names.js";
 
 // ── Ty → Lean type string ──────────────────────────────────
 
@@ -194,9 +194,16 @@ let _unknownEmitted = false;  // across files in one run — the def file import
 // and stays in the more proof-friendly Prop form.
 let _boolCtx = false;
 
+/** Constructor names come from source strings (string-union values,
+ *  discriminated-union tags) and may contain non-identifier characters
+ *  ("spec-pure"); guillemet-quote those — exact and collision-free. */
+function leanCtorName(name: string): string {
+  return /^[A-Za-z_][A-Za-z0-9_'!?]*$/.test(name) ? name : `«${name}»`;
+}
+
 /** Render a match pattern to Lean syntax: `_`, `.none`, `.some x`, `.syn seq`. */
 function renderLeanPattern(p: MatchPattern): string {
-  return p.kind === "wild" ? "_" : "." + [p.ctor, ...p.binders].join(" ");
+  return p.kind === "wild" ? "_" : "." + [leanCtorName(p.ctor), ...p.binders].join(" ");
 }
 
 // A Bool-valued atom that does NOT coerce to Prop: an inlined union discriminator
@@ -304,7 +311,7 @@ function emitExpr(e: Expr, parentPrec?: number): string {
       // like `match ... | .none => Type.some x` where elaboration can't infer).
       // Without type: emit `.name` (dotted form; works in pattern positions
       // and where the expected type is clear from context).
-      const head = e.type ? `${e.type}.${e.name}` : `.${e.name}`;
+      const head = e.type ? `${e.type}.${leanCtorName(e.name)}` : `.${leanCtorName(e.name)}`;
       if (!e.args || e.args.length === 0) return head;
       const args = e.args.map(a =>
         (a.kind === "binop" || a.kind === "unop" || a.kind === "implies" || a.kind === "app" || a.kind === "methodCall") ? `(${emitExpr(a)})` : emitExpr(a)
@@ -407,7 +414,10 @@ function emitExpr(e: Expr, parentPrec?: number): string {
       // Datatype constructor (tagged by transform): Lean needs the qualified name
       // `BaseType.variant`; a bare `variant` is an unknown identifier. (Dafny keeps
       // the bare form, so its output is unaffected.)
-      if (e.ctorOf) return args.length ? `${e.ctorOf}.${e.fn} ${args.join(" ")}` : `${e.ctorOf}.${e.fn}`;
+      if (e.ctorOf) {
+        const ctor = leanCtorName(e.fn);
+        return args.length ? `${e.ctorOf}.${ctor} ${args.join(" ")}` : `${e.ctorOf}.${ctor}`;
+      }
       // Option constructors arrive Dafny-spelled from transform (`app "Some"`);
       // Lean core exports the lowercase forms as top-level names.
       if (e.fn === "Some" && args.length === 1) return `some ${args[0]}`;
@@ -486,7 +496,7 @@ function emitExpr(e: Expr, parentPrec?: number): string {
       // so any token after an arm body (`→`, another match's `|`, etc.) would
       // bleed into the last `.none` case without explicit bracketing.
       const arms = e.arms.map(a => `| ${renderLeanPattern(a.pattern)} => ${emitExpr(a.body)}`);
-      const scrut = typeof e.scrutinee === "string" ? e.scrutinee : emitExpr(e.scrutinee);
+      const scrut = emitExpr(e.scrutinee);
       return `(match ${scrut} with ${arms.join(" ")})`;
     }
 
@@ -579,7 +589,7 @@ function emitStmt(s: Stmt, indent: number): string {
     }
 
     case "match": {
-      const scrut = typeof s.scrutinee === "string" ? s.scrutinee : emitExpr(s.scrutinee);
+      const scrut = emitExpr(s.scrutinee);
       // Option match (.some/.none) → emit as if/let for WPGen.if compatibility
       if (s.arms.length === 2) {
         const someArm = s.arms.find(a => a.pattern.kind === "ctor" && a.pattern.ctor === "some");
@@ -697,10 +707,10 @@ function emitDecl(d: Decl): string {
       const lines = [`inductive ${d.name} where`];
       for (const c of d.constructors) {
         if (c.fields.length === 0) {
-          lines.push(`  | ${c.name} : ${d.name}`);
+          lines.push(`  | ${leanCtorName(c.name)} : ${d.name}`);
         } else {
           const params = c.fields.map(f => `(${escapeName(f.name)} : ${tyToLean(f.type)})`).join(" ");
-          lines.push(`  | ${c.name} ${params} : ${d.name}`);
+          lines.push(`  | ${leanCtorName(c.name)} ${params} : ${d.name}`);
         }
       }
       return lines.join("\n") + emitDeriving(d.name, d.deriving);
@@ -757,7 +767,7 @@ function emitDecl(d: Decl): string {
       // Prime the return binder only on a collision within *this method's own*
       // signature/body — `res` is a common identifier module-wide (record
       // fields, unrelated params), so a module-wide check would prime spuriously.
-      _resultName = freshName("res", n =>
+      _resultName = freshNameWhere("res", n =>
         d.params.some(p => escapeName(p.name) === n) ||
         usesNameInDecl(d.requires, d.ensures, d.body, n));
       const lines = [`method ${d.name} ${params} return (${_resultName} : ${tyToLean(d.returnType)})`];
@@ -813,7 +823,7 @@ function emitPureExpr(e: Expr, indent: number): string {
     case "if":
       return `${pad}if ${emitExpr(e.cond)} then\n${emitPureExpr(e.then, indent + 1)}\n${pad}else\n${emitPureExpr(e.else, indent + 1)}`;
     case "match": {
-      const lines = [`${pad}match ${typeof e.scrutinee === "string" ? e.scrutinee : emitExpr(e.scrutinee)} with`];
+      const lines = [`${pad}match ${emitExpr(e.scrutinee)} with`];
       for (const arm of e.arms) {
         lines.push(`${pad}| ${renderLeanPattern(arm.pattern)} =>`);
         lines.push(emitPureExpr(arm.body, indent + 1));
diff --git a/tools/src/names.ts b/tools/src/names.ts
index 1647619..063d44e 100644
--- a/tools/src/names.ts
+++ b/tools/src/names.ts
@@ -44,12 +44,17 @@ export function userNames(): readonly string[] {
   return [..._userNames];
 }
 
-/** A toolchain-internal name: `base` verbatim, primed on collision. The one
- *  place the priming rule lives. `taken` says what counts as a collision —
- *  by default a user-written name anywhere in the module; callers that know
- *  the exact scope (e.g. a comprehension binder checking only the expressions
- *  it wraps) pass their own predicate. */
-export function freshName(base: string, taken: (name: string) => boolean = isUserName): string {
+/** A toolchain-internal name: `base` verbatim, primed on collision against
+ *  user-written names anywhere in the module. The common form — deterministic
+ *  per module. */
+export function freshName(base: string): string {
+  return freshNameWhere(base, isUserName);
+}
+
+/** The priming rule, against a caller-chosen collision predicate — for
+ *  callers that know the exact scope (e.g. a comprehension binder checking
+ *  only the expressions it wraps). The one place the rule lives. */
+export function freshNameWhere(base: string, taken: (name: string) => boolean): string {
   let name = base;
   while (taken(name)) name += "'";
   return name;
diff --git a/tools/src/peephole.ts b/tools/src/peephole.ts
index 040e4ea..de4a0a6 100644
--- a/tools/src/peephole.ts
+++ b/tools/src/peephole.ts
@@ -14,7 +14,7 @@
  * Statement-level rule 1 also handles match-statement on m.get.
  */
 import type { Expr, Stmt, Decl, Module, MatchArm, StmtMatchArm, MatchPattern } from "./ir.js";
-import { patternCtor, patternBinders } from "./ir.js";
+import { patternCtor, patternBinders, usesName, usesNameInStmts } from "./ir.js";
 
 // ── Generic walkers (same shape as transform.ts) ─────────────
 
@@ -40,7 +40,7 @@ function mapExpr(e: Expr, f: (e: Expr) => Expr | null): Expr {
     case "arrayLiteral": return { ...e, elems: e.elems.map(r) };
     case "if": return { ...e, cond: r(e.cond), then: r(e.then), else: r(e.else) };
     case "match": {
-      const scr = typeof e.scrutinee === "string" ? e.scrutinee : r(e.scrutinee);
+      const scr = r(e.scrutinee);
       return { ...e, scrutinee: scr, arms: e.arms.map(a => ({ ...a, body: r(a.body) })) };
     }
     case "forall": return { ...e, body: r(e.body) };
@@ -87,7 +87,7 @@ function getSomeNoneArms<A extends { pattern: MatchPattern; body: any }>(arms: A
  *  Bind once (let-expression) rather than substitute, so the verifier doesn't
  *  re-derive `k in m` at every use of v inside sb. */
 function ruleMatchOnMapGetExpr(e: Expr): Expr | null {
-  if (e.kind !== "match" || typeof e.scrutinee === "string") return null;
+  if (e.kind !== "match") return null;
   const get = isMapGet(e.scrutinee);
   if (!get) return null;
   const arms = getSomeNoneArms(e.arms);
@@ -138,14 +138,12 @@ function ruleLetMatchOnMapGetExpr(e: Expr): Expr | null {
   if (!get) return null;
   if (e.body.kind !== "match") return null;
   const m = e.body;
-  const matchOnX =
-    (typeof m.scrutinee === "string" && m.scrutinee === e.name) ||
-    (typeof m.scrutinee !== "string" && m.scrutinee.kind === "var" && m.scrutinee.name === e.name);
+  const matchOnX = m.scrutinee.kind === "var" && m.scrutinee.name === e.name;
   if (!matchOnX) return null;
   const arms = getSomeNoneArms(m.arms);
   if (!arms) return null;
   // x must not appear in arm bodies (otherwise the binding is needed)
-  if (containsVarRefExpr(arms.someArm.body, e.name) || containsVarRefExpr(arms.noneArm.body, e.name)) return null;
+  if (usesName(arms.someArm.body, e.name) || usesName(arms.noneArm.body, e.name)) return null;
   const idx: Expr = { kind: "index", arr: get.obj, idx: get.key };
   const someBody: Expr = arms.binder
     ? { kind: "let", name: arms.binder, value: idx, body: arms.someArm.body }
@@ -154,16 +152,6 @@ function ruleLetMatchOnMapGetExpr(e: Expr): Expr | null {
   return { kind: "if", cond: has, then: someBody, else: arms.noneArm.body };
 }
 
-function containsVarRefExpr(e: Expr, name: string): boolean {
-  let found = false;
-  mapExpr(e, x => {
-    if (found) return x;
-    if (x.kind === "var" && x.name === name) { found = true; return x; }
-    return null;
-  });
-  return found;
-}
-
 function isBool(e: Expr, v: boolean): boolean {
   return e.kind === "bool" && e.value === v;
 }
@@ -194,7 +182,7 @@ let EXPR_RULES: ((e: Expr) => Expr | null)[] = [...MAP_GET_RULES, ...BOOL_RULES]
  *  Bind once (var declaration) rather than substitute — substituting would
  *  re-evaluate m[k] at every use, changing semantics if the body mutates m. */
 function ruleMatchOnMapGetStmt(s: Stmt): Stmt | null {
-  if (s.kind !== "match" || typeof s.scrutinee === "string") return null;
+  if (s.kind !== "match") return null;
   const get = isMapGet(s.scrutinee);
   if (!get) return null;
   const arms = getSomeNoneArms(s.arms);
@@ -212,57 +200,6 @@ const STMT_RULES = [ruleMatchOnMapGetStmt];
 
 // ── Variable use detection ───────────────────────────────────
 
-/** Conservative reference check: does any expression in this stmt mention `name`?
- *  Doesn't track shadowing — worst case, we miss an inlining opportunity.
- *  Used to gate let-inlining (only inline if the var is not used anywhere after). */
-function containsVarRefStmt(s: Stmt, name: string): boolean {
-  let found = false;
-  const checkExpr = (e: Expr) => {
-    if (found) return;
-    mapExpr(e, x => {
-      if (x.kind === "var" && x.name === name) { found = true; return x; }
-      return null;
-    });
-  };
-  const walk = (st: Stmt): void => {
-    if (found) return;
-    switch (st.kind) {
-      case "let": case "assign": case "bind": case "let-bind":
-      case "return": case "ghostLet": case "ghostAssign":
-        checkExpr(st.value); return;
-      case "assert": checkExpr(st.expr); return;
-      case "break": case "continue": return;
-      case "if":
-        checkExpr(st.cond);
-        st.then.forEach(walk); st.else.forEach(walk); return;
-      case "match":
-        if (typeof st.scrutinee === "string") {
-          if (st.scrutinee === name) { found = true; return; }
-        } else {
-          checkExpr(st.scrutinee);
-        }
-        st.arms.forEach(a => a.body.forEach(walk));
-        return;
-      case "while":
-        checkExpr(st.cond);
-        st.invariants.forEach(checkExpr);
-        st.body.forEach(walk);
-        return;
-      case "forin":
-        checkExpr(st.bound);
-        st.invariants.forEach(checkExpr);
-        st.body.forEach(walk);
-        return;
-    }
-  };
-  walk(s);
-  return found;
-}
-
-function containsVarRefStmts(stmts: Stmt[], name: string): boolean {
-  return stmts.some(s => containsVarRefStmt(s, name));
-}
-
 // ── Statement-list rules (pairs of adjacent stmts) ──────────
 
 /** Pair rule: let x = m.get(k); match x { Some(v) => sb, None => nb }
@@ -274,13 +211,11 @@ function tryLetMatchOnMapGet(s1: Stmt, s2: Stmt, restStmts: Stmt[]): Stmt | null
   const get = isMapGet(s1.value);
   if (!get) return null;
   if (s2.kind !== "match") return null;
-  const matchOnX =
-    (typeof s2.scrutinee === "string" && s2.scrutinee === s1.name) ||
-    (typeof s2.scrutinee !== "string" && s2.scrutinee.kind === "var" && s2.scrutinee.name === s1.name);
+  const matchOnX = s2.scrutinee.kind === "var" && s2.scrutinee.name === s1.name;
   if (!matchOnX) return null;
   const arms = getSomeNoneArms(s2.arms);
   if (!arms) return null;
-  if (containsVarRefStmts(restStmts, s1.name)) return null;
+  if (usesNameInStmts(restStmts, s1.name)) return null;
   const idx: Expr = { kind: "index", arr: get.obj, idx: get.key };
   const valTy = get.objTy.kind === "map" ? get.objTy.value : { kind: "unknown" as const };
   const someBody: Stmt[] = arms.binder
@@ -358,7 +293,7 @@ function rewriteChildrenExpr(e: Expr): Expr {
     case "arrayLiteral": return { ...e, elems: e.elems.map(r) };
     case "if": return { ...e, cond: r(e.cond), then: r(e.then), else: r(e.else) };
     case "match": {
-      const scr = typeof e.scrutinee === "string" ? e.scrutinee : r(e.scrutinee);
+      const scr = r(e.scrutinee);
       return { ...e, scrutinee: scr, arms: e.arms.map(a => ({ ...a, body: r(a.body) })) };
     }
     case "forall": return { ...e, body: r(e.body) };
@@ -399,7 +334,7 @@ function rewriteChildrenStmt(s: Stmt): Stmt {
     case "break": case "continue": return s;
     case "if": return { ...s, cond: re(s.cond), then: rs(s.then), else: rs(s.else) };
     case "match": {
-      const scr = typeof s.scrutinee === "string" ? s.scrutinee : re(s.scrutinee);
+      const scr = re(s.scrutinee);
       return { ...s, scrutinee: scr, arms: s.arms.map(a => ({ ...a, body: rs(a.body) })) };
     }
     case "while": return { ...s, cond: re(s.cond), invariants: s.invariants.map(re), body: rs(s.body) };
diff --git a/tools/src/resolve.ts b/tools/src/resolve.ts
index 063981e..1cd4ca0 100644
--- a/tools/src/resolve.ts
+++ b/tools/src/resolve.ts
@@ -14,7 +14,7 @@ import { parseExpr } from "./specparser.js";
 import { freshName } from "./names.js";
 import { recognizeBuiltin, builtinSpec } from "./builtins.js";
 import { declOf, declOfKind, declOfDotted, declOfTy, tyBaseName } from "./typedecls.js";
-import { presentFact } from "./condition-facts.js";
+import { presentFact, variantFact } from "./condition-facts.js";
 
 // ── Environment ──────────────────────────────────────────────
 
@@ -69,6 +69,7 @@ function accessPathsEqual(a: AccessPath, b: AccessPath): boolean {
 interface NarrowedPath {
   path: AccessPath;
   narrowedTy: Ty;
+  variant?: string;   // union variant the path is narrowed to (discriminant check)
 }
 
 /** A `k in m` atom known to hold in the current scope. Both sides are pure
@@ -187,6 +188,18 @@ function collectEarlyReturnNarrowings(cond: TExpr): { varName: string; innerTy:
   return n ? [n] : [];
 }
 
+/** Negated discriminant check (`path.kind !== "lit"`) on a var or field path.
+ *  After `if (path.kind !== "lit") return`, the rest of the block knows the
+ *  path is that variant. */
+function negatedVariantCheck(cond: TExpr): NarrowedPath | null {
+  if (cond.kind === "binop" && cond.op === "!==" && cond.right.kind === "str" &&
+      cond.left.kind === "field" && cond.left.isDiscriminant && cond.left.obj.ty.kind === "user") {
+    const path = asTExprAccessPath(cond.left.obj);
+    if (path) return { path, narrowedTy: cond.left.obj.ty, variant: cond.right.value };
+  }
+  return null;
+}
+
 /** TExpr → AccessPath. Counterpart to `asRawAccessPath` for resolved trees.
  *  Used by `extractInAtoms` when pulling atoms out of typed spec expressions. */
 function asTExprAccessPath(e: TExpr): AccessPath | null {
@@ -253,13 +266,24 @@ function collectAndChainNarrowings(cond: TExpr, ctx: Ctx): Ctx {
     return collectAndChainNarrowings(cond.right, leftCtx);
   }
   const f = presentFact(cond);
-  if (!f || f.negated) return ctx;
-  if (f.scrutinee.kind === "var") {
-    return withEnv(ctx, extend(ctx.env, f.scrutinee.name, f.innerTy));
+  if (f && !f.negated) {
+    if (f.scrutinee.kind === "var") {
+      return withEnv(ctx, extend(ctx.env, f.scrutinee.name, f.innerTy));
+    }
+    const path = asTExprAccessPath(f.scrutinee);
+    if (path) {
+      return { ...ctx, narrowedPaths: [...ctx.narrowedPaths, { path, narrowedTy: f.innerTy }] };
+    }
+    return ctx;
   }
-  const path = asTExprAccessPath(f.scrutinee);
-  if (path) {
-    return { ...ctx, narrowedPaths: [...ctx.narrowedPaths, { path, narrowedTy: f.innerTy }] };
+  // Positive discriminant check (`x.kind === "bool"`): record the variant so
+  // field reads on the path resolve against that variant's field types.
+  const vf = variantFact(cond, { decls: ctx.typeDecls, oc: { n: 0 } });
+  if (vf) {
+    const path = asTExprAccessPath(vf.scrutinee);
+    if (path) {
+      return { ...ctx, narrowedPaths: [...ctx.narrowedPaths, { path, narrowedTy: vf.scrutinee.ty, variant: vf.variant }] };
+    }
   }
   return ctx;
 }
@@ -410,6 +434,7 @@ function classifyCall(fn: RawExpr, ctx: Ctx): CallKind {
   // don't get lifted to statement-level binds (which would force lambdas to
   // become multi-statement, illegal in Dafny).
   if (fn.kind === "var" && ctx.externs.has(fn.name)) return "pure";
+  if (fn.kind === "var" && lookup(ctx.env, fn.name)?.kind === "fn") return "pure";
   if (fn.kind === "var" && ctx.inSpec) {
     // Not a known pure function — could be external (Lean-defined spec helper).
     // Pass through as "pure" and let Lean catch any errors.
@@ -820,6 +845,11 @@ function resolveExpr(e: RawExpr, ctx: Ctx): TExpr {
       if (ty.kind === "unknown" && fn.kind === "var" && ctx.fnReturns.has(fn.name)) {
         ty = ctx.fnReturns.get(fn.name)!;
       }
+      // Call through a function-typed value: its fn type carries the result
+      if (ty.kind === "unknown" && fn.kind === "var") {
+        const varTy = lookup(ctx.env, fn.name);
+        if (varTy?.kind === "fn") ty = varTy.result;
+      }
       // filterMap: `seqOfOption.filter(x => x !== undefined)` (a defined-check,
       // typically with an `x is T` type guard) drops the Nones AND unwraps to
       // seq<T>. Rewrite to a synthetic `filterSome` call lowered to the proven
@@ -885,23 +915,41 @@ function resolveExpr(e: RawExpr, ctx: Ctx): TExpr {
         }
       }
 
+      // A variant narrowing on the object picks the field's type from that
+      // variant (a shared field name can have a different type per variant).
+      let ofVariant: string | undefined;
+      if (ty.kind === "unknown" && ctx.narrowedPaths.length > 0 && obj.ty.kind === "user") {
+        const objPath = asRawAccessPath(e.obj);
+        const np = objPath ? ctx.narrowedPaths.find(n => n.variant && accessPathsEqual(n.path, objPath)) : undefined;
+        if (np?.variant) {
+          const decl = findDecl(ctx, tyBaseName(obj.ty.name));
+          const f = decl?.variants?.find(v => v.name === np.variant)?.fields.find(f => f.name === e.field);
+          if (f?.type) { ty = f.type; ofVariant = np.variant; }
+        }
+      }
+
       if (ty.kind === "unknown") {
         const lookup = lookupFieldTy(obj.ty, e.field, ctx);
         ty = lookup.ty;
         isDiscriminant = lookup.isDiscriminant;
       }
 
-      return { kind: "field", obj, field: e.field, ty, isDiscriminant };
+      return { kind: "field", obj, field: e.field, ty, isDiscriminant, ofVariant };
     }
 
     case "nullish": {
       // left ?? right — result type is left's inner (when left is optional)
       // or just left's type, unified with right's type.
       const left = resolveExpr(e.left, ctx);
-      const ty: Ty = left.ty.kind === "optional" ? left.ty.inner : left.ty;
+      const inner: Ty = left.ty.kind === "optional" ? left.ty.inner : left.ty;
       // The default shares the result type, so coerce a string literal to a
       // string-union enum (e.g. `availableLevels[0] ?? "off"`).
-      const right = coerceStr(resolveExpr(e.right, ctx), ty);
+      const right = coerceStr(resolveExpr(e.right, ctx), inner);
+      // `??` is only total when its default is: with a nullable right operand
+      // (rule-chain style `ruleA(e) ?? ruleB(e) ?? null`), the result stays
+      // optional — otherwise the enclosing chain level loses its optionality
+      // and narrowing can't rewrite it.
+      const ty: Ty = right.ty.kind === "optional" ? right.ty : inner;
       return { kind: "nullish", left, right, ty };
     }
 
@@ -978,14 +1026,32 @@ function resolveExpr(e: RawExpr, ctx: Ctx): TExpr {
       const returnTyUnwrapped = ctx.returnTy.kind === "optional" ? ctx.returnTy.inner : ctx.returnTy;
       const recordTy = ty.kind === "user" ? ty : returnTyUnwrapped.kind === "user" ? returnTyUnwrapped : null;
       const decl = recordTy ? declOfKind(ctx.typeDecls, recordTy.name, "record") : undefined;
+      // Union-variant literal in union-typed context (a constructed IR node,
+      // `{ kind: "if", … }: TStmt`): contextual field types come from the
+      // variant the literal's discriminant field selects.
+      let declFields = decl?.fields;
+      if (!declFields && recordTy) {
+        const udecl = declOfKind(ctx.typeDecls, recordTy.name, "discriminated-union");
+        if (udecl?.discriminant && udecl.variants) {
+          const tagRaw = e.fields.find(f => f.name === udecl.discriminant)?.value;
+          if (tagRaw?.kind === "str") {
+            declFields = udecl.variants.find(v => v.name === tagRaw.value)?.fields;
+          }
+        }
+      }
       // Clear returnTy for field values — it applies to THIS record, not nested ones
       const fieldCtx = recordTy ? { ...ctx, returnTy: { kind: "unknown" as const } as Ty } : ctx;
       const fields = e.fields.map(f => {
-        const fieldDecl = decl?.fields?.find(df => df.name === f.name);
+        const fieldDecl = declFields?.find(df => df.name === f.name);
         // Propagate declared field type into context so nested records resolve
-        // their union variant correctly (e.g., { kind: 'Idle' } → EffectMode.Idle)
-        const valueCtx = (fieldDecl?.type?.kind === "user")
-          ? { ...fieldCtx, returnTy: fieldDecl.type }
+        // their union variant correctly (e.g., { kind: 'Idle' } → EffectMode.Idle).
+        // Optional fields propagate their inner type (the Some-wrap is restored
+        // by coerceToTargetTy below); array fields propagate whole, so the
+        // arrayLiteral case can thread the element type.
+        const fdTy = fieldDecl?.type;
+        const fdCtxTy = fdTy?.kind === "optional" ? fdTy.inner : fdTy;
+        const valueCtx = fdCtxTy && (fdCtxTy.kind === "user" || fdCtxTy.kind === "array")
+          ? { ...fieldCtx, returnTy: fdCtxTy }
           : fieldCtx;
         let value = resolveExpr(f.value, valueCtx);
         if (fieldDecl) {
@@ -1043,8 +1109,10 @@ function resolveExpr(e: RawExpr, ctx: Ctx): TExpr {
       // literal in an array resolves to its named datatype rather than an
       // anonymous tuple (mirrors return-position and call-argument records, which
       // get their type via ctx.returnTy). Only narrow when the context type is an
-      // array; otherwise leave ctx untouched.
-      const expectedElem = ctx.returnTy.kind === "array" ? ctx.returnTy.elem : null;
+      // array (unwrapping one optional level — `TStmt[] | null` return positions);
+      // otherwise leave ctx untouched.
+      const rtUnwrapped = ctx.returnTy.kind === "optional" ? ctx.returnTy.inner : ctx.returnTy;
+      const expectedElem = rtUnwrapped.kind === "array" ? rtUnwrapped.elem : null;
       const elemCtx = expectedElem ? { ...ctx, returnTy: expectedElem } : ctx;
       const elems = e.elems.map(el => {
         const r = resolveExpr(el, elemCtx);
@@ -1176,8 +1244,9 @@ function resolveBlock(stmts: RawStmt[], ctx: Ctx): TStmt[] {
   const result: TStmt[] = [];
   let env = ctx.env;
   let narrowedIndices = ctx.narrowedIndices;
+  let narrowedPaths = ctx.narrowedPaths;
   for (const s of stmts) {
-    const currentCtx = { ...ctx, env, narrowedIndices };
+    const currentCtx = { ...ctx, env, narrowedIndices, narrowedPaths };
     const [typed, nextEnv] = resolveStmt(s, currentCtx);
     result.push(typed);
     env = nextEnv;
@@ -1193,6 +1262,8 @@ function resolveBlock(stmts: RawStmt[], ctx: Ctx): TStmt[] {
         for (const n of collectEarlyReturnNarrowings(typed.cond)) {
           env = extend(env, n.varName, n.innerTy);
         }
+        const nv = negatedVariantCheck(typed.cond);
+        if (nv) narrowedPaths = [...narrowedPaths, nv];
       }
       // Map-index narrowing: `if (!(k in m)) return;` means `k in m` holds in rest.
       if (typed.kind === "if") {
@@ -1230,8 +1301,11 @@ function resolveStmt(s: RawStmt, ctx: Ctx): [TStmt, Env | null] {
       // Propagate declared type as returnTy so nested record expressions resolve
       // union variants correctly (e.g., EffectState → mode: EffectMode → { kind:
       // 'Idle' }). Arrays too, so `const xs: Foo[] = [{...}]` threads the element
-      // type into the array literal (see the arrayLiteral case).
-      const initCtx = (declTy.kind === "user" || declTy.kind === "array") ? { ...ctx, returnTy: declTy } : ctx;
+      // type into the array literal (see the arrayLiteral case). Optionals too
+      // (`const r: TExpr | null = cond ? {…} : null`) — the record case unwraps
+      // one optional level when consulting returnTy.
+      const initCtx = (declTy.kind === "user" || declTy.kind === "array" || declTy.kind === "optional")
+        ? { ...ctx, returnTy: declTy } : ctx;
       const init = coerceStr(resolveExpr(s.init, initCtx), declTy);
       let ty: Ty;
       if (isUnmodeledTy(declTy, ctx.typeDecls) && !isUnmodeledTy(init.ty, ctx.typeDecls)) {
@@ -1262,7 +1336,12 @@ function resolveStmt(s: RawStmt, ctx: Ctx): [TStmt, Env | null] {
 
     case "assign": {
       const targetTy = lookup(ctx.env, s.target) ?? { kind: "unknown" as const };
-      let value = coerceStr(resolveExpr(s.value, ctx), targetTy);
+      // Propagate the target's type as returnTy, mirroring the annotated-let
+      // case, so record/union literals and array literals in the RHS resolve
+      // to their named datatypes.
+      const valueCtx = (targetTy.kind === "user" || targetTy.kind === "array" || targetTy.kind === "optional")
+        ? { ...ctx, returnTy: targetTy } : ctx;
+      let value = coerceStr(resolveExpr(s.value, valueCtx), targetTy);
       // Auto-wrap non-optional value in Some when target is optional
       const isUndef = value.kind === "var" && value.name === "undefined";
       if (targetTy.kind === "optional" && value.ty.kind !== "optional" && value.ty.kind !== "unknown" && !isUndef) {
diff --git a/tools/src/transform.ts b/tools/src/transform.ts
index 08e5354..a808644 100644
--- a/tools/src/transform.ts
+++ b/tools/src/transform.ts
@@ -6,9 +6,10 @@
  */
 
 import type { TExpr, TStmt, TFunction, TModule, Ty } from "./typedir.js";
+import { tyEqual } from "./typedir.js";
 import type { Expr, Stmt, Decl, Module, FnDef, FnDefByMethod, FnMethod, MatchArm, StmtMatchArm, ConstDecl, MatchPattern } from "./ir.js";
 import { anyExprInStmts, pWild, pCtor, patternBinders, patternBinds, patternCtor } from "./ir.js";
-import type { TypeDeclInfo } from "./types.js";
+import type { TypeDeclInfo, VariantInfo } from "./types.js";
 import { parseTsType } from "./types.js";
 import { freshName } from "./names.js";
 import { builtinSpec } from "./builtins.js";
@@ -44,7 +45,7 @@ function mapExpr(e: Expr, f: (e: Expr) => Expr | null): Expr {
     case "arrayLiteral": return { ...e, elems: e.elems.map(r) };
     case "if": return { ...e, cond: r(e.cond), then: r(e.then), else: r(e.else) };
     case "match": {
-      const scr = typeof e.scrutinee === "string" ? e.scrutinee : r(e.scrutinee);
+      const scr = r(e.scrutinee);
       return { ...e, scrutinee: scr, arms: e.arms.map(a => ({ ...a, body: r(a.body) })) };
     }
     case "forall": return { ...e, body: r(e.body) };
@@ -67,7 +68,7 @@ function mapStmt(s: Stmt, f: (e: Expr) => Expr | null): Stmt {
     case "break": case "continue": return s;
     case "if": return { ...s, cond: r(s.cond), then: s.then.map(t => mapStmt(t, f)), else: s.else.map(t => mapStmt(t, f)) };
     case "match": {
-      const scr = typeof s.scrutinee === "string" ? s.scrutinee : r(s.scrutinee);
+      const scr = r(s.scrutinee);
       return { ...s, scrutinee: scr, arms: s.arms.map(a => ({ ...a, body: a.body.map(t => mapStmt(t, f)) })) };
     }
     case "while": return { ...s, cond: r(s.cond), invariants: s.invariants.map(r), body: s.body.map(t => mapStmt(t, f)) };
@@ -86,6 +87,7 @@ function mapStmt(s: Stmt, f: (e: Expr) => Expr | null): Stmt {
  *  walks them by hand — statement binders are tracked only at that body's top
  *  level, which is enough for the sole caller (dafny-emit's
  *  `comprehensionBinder`). TODO: generalize if more callers need this. */
+const varE = (name: string): Expr => ({ kind: "var", name });
 export function renameFreeVar(e: Expr, from: string, to: string): Expr {
   const f = (x: Expr): Expr | null => {
     if (x.kind === "var") return x.name === from ? { ...x, name: to } : x;
@@ -94,9 +96,7 @@ export function renameFreeVar(e: Expr, from: string, to: string): Expr {
     if (x.kind === "let" && x.name === from) return { ...x, value: mapExpr(x.value, f) };
     if ((x.kind === "forall" || x.kind === "exists") && x.var === from) return x;
     if (x.kind === "match") {
-      const scr = typeof x.scrutinee === "string"
-        ? (x.scrutinee === from ? to : x.scrutinee) : mapExpr(x.scrutinee, f);
-      return { ...x, scrutinee: scr, arms: x.arms.map(a =>
+      return { ...x, scrutinee: mapExpr(x.scrutinee, f), arms: x.arms.map(a =>
         patternBinds(a.pattern, from) ? a : { ...a, body: mapExpr(a.body, f) }) };
     }
     if (x.kind === "lambda") {
@@ -202,6 +202,36 @@ let _typeDecls: TypeDeclInfo[] = [];
  *  redirected to the pure mirror. Set once per module transform. */
 let _pureDefNames: Set<string> = new Set();
 
+/** Discriminated unions whose tag is read as a *value* (`x.kind` compared
+ *  to another union's tag, passed as an argument, …). Each gets a generated
+ *  `<Union>_<disc>` discriminator function beside its datatype, returning
+ *  the source tag strings. Narrowing consumes discriminant *checks*, so this
+ *  fires only for surviving reads. Populated during body transforms; drained
+ *  into the types file. */
+let _neededKindHelpers = new Map<string, TypeDeclInfo>();
+
+function kindHelperName(decl: TypeDeclInfo): string {
+  return freshName(`${decl.name}_${decl.discriminant}`);
+}
+
+function kindHelperDecl(decl: TypeDeclInfo): Decl {
+  return {
+    kind: "def",
+    name: kindHelperName(decl),
+    typeParams: [],
+    params: [{ name: "t", type: { kind: "user", name: decl.name } }],
+    returnType: { kind: "string" },
+    requires: [], ensures: [], decreases: null,
+    body: {
+      kind: "match", scrutinee: varE("t"),
+      arms: decl.variants!.map(v => ({
+        pattern: { kind: "ctor" as const, ctor: v.name, binders: v.fields.map((_, i) => `_${i}`) },
+        body: { kind: "str" as const, value: v.name },
+      })),
+    },
+  };
+}
+
 /** Prefix match-bound field names to avoid capturing user variables.
  *  When prefix is given (the scrutinee name), include it to avoid
  *  collisions in nested matches on different variables. `freshName` closes
@@ -357,7 +387,7 @@ function wrapOptionalBranch(expr: Expr, raw: TExpr): Expr {
   // The dotted form `.some`/`.none` would be ambiguous in expression positions
   // like the scrutinee of an outer match. Dafny treats `Option.Some` and bare
   // `Some` equivalently — the qualification is harmless there.
-  if (raw.kind === "var" && raw.name === "undefined") return { kind: "constructor", name: "none", type: "Option" };
+  if (raw.kind === "var" && raw.name === "undefined") return { kind: "constructor", name: "none", type: "Option", args: [] };
   if (raw.ty.kind === "optional") return expr;  // already Option<T>, don't double-wrap
   return { kind: "constructor", name: "some", type: "Option", args: [expr] };
 }
@@ -419,7 +449,7 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
     case "bool": return { kind: "bool", value: e.value };
 
     case "str":
-      if (e.ty.kind === "user") return { kind: "constructor", name: e.value, type: e.ty.name };
+      if (e.ty.kind === "user") return { kind: "constructor", name: e.value, type: e.ty.name, args: [] };
       return { kind: "str", value: e.value };
 
     case "unop":
@@ -468,7 +498,7 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
           kind: "binop",
           op: e.op === "===" ? "=" : "≠",
           left: transformExpr(e.left.obj),
-          right: { kind: "constructor", name: e.right.value, type: objTy },
+          right: { kind: "constructor", name: e.right.value, type: objTy, args: [] },
         };
       }
       // String literal comparison — constructor if user type, string literal if string.
@@ -478,7 +508,7 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
         const left = lowerExpr(e.left, binds);
         const leftTy = e.left.ty.kind === "user" ? e.left.ty.name : undefined;
         const right: Expr = isUser(e.left.ty)
-          ? { kind: "constructor", name: e.right.value, type: leftTy }
+          ? { kind: "constructor", name: e.right.value, type: leftTy, args: [] }
           : { kind: "str", value: e.right.value };
         return { kind: "binop", op: e.op === "===" ? "=" : "≠", left, right };
       }
@@ -503,7 +533,7 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
         // non-optional string-literal rule above.
         const innerTy = optSide.ty.kind === "optional" ? optSide.ty.inner : optSide.ty;
         const valExpr: Expr = valSide.kind === "str" && innerTy.kind === "user"
-          ? { kind: "constructor", name: valSide.value, type: innerTy.name }
+          ? { kind: "constructor", name: valSide.value, type: innerTy.name, args: [] }
           : lowerExpr(valSide, binds);
         const cmpOp = BOOL_OP_MAP[e.op] ?? e.op;
         const noneVal = e.op === "!==" ? true : false;
@@ -692,6 +722,15 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
         if (decl?.variants?.some(v => v.name === "true")) {
           return { kind: "field", obj: transformExpr(e.obj), field: "true_?" };
         }
+        // Surviving string-discriminant read (`x.kind` used as a value —
+        // compared against another union's tag, passed as an argument, …):
+        // lower to the generated per-union discriminator function, which
+        // returns the source tag strings. Narrowing consumes discriminant
+        // *checks*; this catches reads that survive as values.
+        if (decl?.variants && decl.discriminant && decl.discriminant !== "__isArray__") {
+          _neededKindHelpers.set(decl.name, decl);
+          return { kind: "app", fn: kindHelperName(decl), args: [lowerExpr(e.obj, binds)] };
+        }
       }
       // Union destructor: `x.field` where x is a discriminated union and `field`
       // is a data field of one of its variants. Dafny reads the destructor
@@ -700,8 +739,20 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
       if (e.obj.ty.kind === "user") {
         const baseName = tyBaseName(e.obj.ty.name);
         const decl = declOfKind(_typeDecls, baseName, "discriminated-union");
-        if (decl?.variants?.some(v => v.fields.some(f => f.name === e.field))) {
-          return { kind: "field", obj: transformExpr(e.obj), field: e.field, fromUnion: baseName, datatypeField: true };
+        const owners = decl?.variants?.filter(v => v.fields.some(f => f.name === e.field)) ?? [];
+        if (owners.length > 0) {
+          // Shared field name with differing declared types: those destructors
+          // are renamed per-constructor, and the read's own resolved type
+          // identifies the owning variant (the types differ exactly when the
+          // rename happens). Pin it so emitters use the renamed destructor.
+          const ownerTy = (v: VariantInfo) => v.fields.find(f => f.name === e.field)?.type;
+          const differ = owners.some(v => {
+            const a = ownerTy(v), b = ownerTy(owners[0]);
+            return a && b && !tyEqual(a, b);
+          });
+          const matching = differ ? owners.filter(v => { const t = ownerTy(v); return t && tyEqual(t, e.ty); }) : [];
+          const ctor = e.ofVariant ?? (matching.length === 1 ? matching[0].name : undefined);
+          return { kind: "field", obj: transformExpr(e.obj), field: e.field, fromUnion: baseName, ctor, datatypeField: true };
         }
       }
       return { kind: "field", obj: transformExpr(e.obj), field: e.field, datatypeField: isRecordType(e.obj.ty) };
@@ -737,7 +788,7 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
             return {
               kind: "binop", op: "=",
               left: lowerExpr(arg, binds),
-              right: { kind: "constructor", name: "ArrayBranch", type: arg.ty.name },
+              right: { kind: "constructor", name: "ArrayBranch", type: arg.ty.name, args: [] },
             };
           }
         }
@@ -852,8 +903,11 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
             const variant = decl.variants?.find(v => v.name === variantName);
             if (variant) {
               const nonDiscFields = e.fields.filter(f => f.name !== decl.discriminant);
-              if (nonDiscFields.length === 0) {
-                return { kind: "constructor", name: variantName, type: tyName };
+              // Bare-constructor shortcut only when the variant truly has no
+              // fields — a variant with only optional fields still needs its
+              // None-filled argument list (`int_(None)`, not `int_`).
+              if (variant.fields.length === 0) {
+                return { kind: "constructor", name: variantName, type: tyName, args: [] };
               }
               // Constructor with args: match variant field order. Emit a bare `app`
               // (Dafny renders `variantName(args)`, a valid unqualified constructor
@@ -978,11 +1032,11 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
 
     case "optChain":
       // Narrow should have rewritten optChain to someMatch.
-      throw new Error(`optChain reached transform — narrow should have rewritten it`);
+      throw new Error(`optChain reached transform — narrow should have rewritten it: ${JSON.stringify(e).slice(0, 400)}`);
 
     case "nullish":
       // Narrow should have rewritten nullish to someMatch.
-      throw new Error(`nullish reached transform — narrow should have rewritten it`);
+      throw new Error(`nullish reached transform — narrow should have rewritten it: ${JSON.stringify(e).slice(0, 300)}`);
 
     case "havoc":
       // Dafny's * only works in var/assign positions — lift to own declaration
@@ -1005,7 +1059,7 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
         // Bare-var shortcut, but route \result through lowerExpr so the
         // lemma-side replaceVar pass can substitute it with the function call.
         scrutinee = path.fields.length === 0 && path.rootVar !== "\\result"
-          ? path.rootVar
+          ? varE(path.rootVar)
           : lowerExpr(e.scrutinee, binds);
       } else {
         // Complex scrutinee — narrow pre-bound the someBody to use the binder directly,
@@ -1046,7 +1100,7 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
         const fields = variant?.fields ?? [];
         let body = lowerExpr(c.body, binds);
         if (varName && fields.length > 0) {
-          body = replaceFieldAccess(body, varName, fields);
+          body = replaceFieldAccess(body, varName, fields, c.variant, tyBaseName(e.typeName));
           if (isSynthArrayUnion && fields.length === 1) {
             body = replaceVarInExpr(body, varName, matchBinder(fields[0].name, varName));
           }
@@ -1064,7 +1118,7 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr {
         if (wrapOpt) body = wrapOptionalBranch(body, e.fallthrough);
         arms.push({ pattern: pWild(), body });
       }
-      return { kind: "match", scrutinee: varName ?? scrutinee, arms };
+      return { kind: "match", scrutinee: varName !== undefined ? varE(varName) : scrutinee, arms };
     }
   }
 }
@@ -1106,17 +1160,25 @@ function ensuresToMatch(e: TExpr, typeDecls: TypeDeclInfo[]): Expr | null {
   let rhs = transformExpr(e.right);
   rhs = replaceFieldAccess(rhs, obj.name, fields);
 
-  return { kind: "match", scrutinee: obj.name, arms: [{ pattern, body: rhs }, { pattern: pWild(), body: { kind: "bool", value: true } }] };
+  return { kind: "match", scrutinee: varE(obj.name), arms: [{ pattern, body: rhs }, { pattern: pWild(), body: { kind: "bool", value: true } }] };
 }
 
-function replaceFieldAccess(e: Expr, varName: string, fields: { name: string; tsType: string }[]): Expr {
+function replaceFieldAccess(e: Expr, varName: string, fields: { name: string; tsType: string }[], ctorName?: string, ctorOf?: string): Expr {
   return mapExpr(e, x => {
     if (x.kind === "field" && x.obj.kind === "var" && x.obj.name === varName) {
       const f = fields.find(f => f.name === x.field);
       if (f) return { kind: "var", name: matchBinder(f.name, varName) };
     }
+    // Datatype update of the scrutinee (`{ ...vn, f: v }`): the arm knows the
+    // variant, so stamp it — emitters need it for per-constructor destructor
+    // names. Recurse manually (returning a node stops mapExpr's own descent).
+    if (ctorName && x.kind === "record" && !x.ctor && x.spread &&
+        x.spread.kind === "var" && x.spread.name === varName) {
+      return { ...x, ctor: ctorName, ctorOf,
+        fields: x.fields.map(f => ({ ...f, value: replaceFieldAccess(f.value, varName, fields, ctorName, ctorOf) })) };
+    }
     // If this let shadows the matched variable, stop replacing in the body
-    if (x.kind === "let" && x.name === varName) return { ...x, value: replaceFieldAccess(x.value, varName, fields) };
+    if (x.kind === "let" && x.name === varName) return { ...x, value: replaceFieldAccess(x.value, varName, fields, ctorName, ctorOf) };
     return null;
   });
 }
@@ -1288,7 +1350,7 @@ function matchToIfChains(stmts: Stmt[]): Stmt[] {
     const decl = firstCtor ? declWithVariant(_typeDecls, firstCtor) : undefined;
     if (!decl) return [{ ...s, arms }]; // not a user union (e.g. Option) — leave as match
 
-    const scrutExpr: Expr = typeof s.scrutinee === "string" ? { kind: "var", name: s.scrutinee } : s.scrutinee;
+    const scrutExpr: Expr = s.scrutinee;
     const defaultArm = arms.find(a => a.pattern.kind === "wild");
     let elseBranch: Stmt[] = defaultArm ? defaultArm.body : [];
     for (let k = ctorArms.length - 1; k >= 0; k--) {
@@ -1305,7 +1367,7 @@ function matchToIfChains(stmts: Stmt[]): Stmt[] {
         ? { kind: "match", scrutinee: scrutExpr, arms: [
             { pattern: pCtor(ctor), body: { kind: "bool", value: true } },
             { pattern: pWild(), body: { kind: "bool", value: false } }] }
-        : { kind: "binop", op: "=", left: scrutExpr, right: { kind: "constructor", name: ctor, type: decl.name } };
+        : { kind: "binop", op: "=", left: scrutExpr, right: { kind: "constructor", name: ctor, type: decl.name, args: [] } };
       // Bind only the constructor-field binders the body actually uses, pinning the
       // owning ctor so the destructor doesn't guess (variants share field names).
       const lets: Stmt[] = [];
@@ -1356,6 +1418,26 @@ function requireDoneWithForBreaks(stmts: Stmt[], fnName: string): void {
   }
 }
 
+/** The forin emission places the index increment at the loop-body end, so a
+ *  surviving `continue` would skip it. Insert the increment immediately
+ *  before every same-scope continue (nested loops own their continues),
+ *  mirroring the C-style-for desugar's discipline. */
+function insertIncrementBeforeContinue(stmts: Stmt[], idxName: string): Stmt[] {
+  const incr: Stmt = { kind: "assign", target: idxName,
+    value: { kind: "binop", op: "+", left: { kind: "var", name: idxName }, right: { kind: "num", value: 1 } } };
+  const walk = (ss: Stmt[]): Stmt[] => {
+    const out: Stmt[] = [];
+    for (const s of ss) {
+      if (s.kind === "continue") { out.push(incr, s); continue; }
+      if (s.kind === "if") { out.push({ ...s, then: walk(s.then), else: walk(s.else) }); continue; }
+      if (s.kind === "match") { out.push({ ...s, arms: s.arms.map(a => ({ ...a, body: walk(a.body) })) }); continue; }
+      out.push(s);
+    }
+    return out;
+  };
+  return walk(stmts);
+}
+
 function eliminateTopLevelContinue(stmts: Stmt[]): Stmt[] {
   const out: Stmt[] = [];
   for (let i = 0; i < stmts.length; i++) {
@@ -1464,7 +1546,8 @@ function transformStmts(stmts: TStmt[], typeDecls: TypeDeclInfo[]): Stmt[] {
       const arrSize: Expr = { kind: "field", obj: seq, field: "size" };
       // Auto-add bound invariant: idx ≤ bound (always true for range loops)
       const boundInv: Expr = { kind: "binop", op: "≤", left: idxVar, right: arrSize };
-      const bodyStmts = eliminateTopLevelContinue(transformStmts(s.body, typeDecls));
+      const bodyStmts = insertIncrementBeforeContinue(
+        eliminateTopLevelContinue(transformStmts(s.body, typeDecls)), idxName);
       result.push({
         kind: "forin", idx: idxName, bound: arrSize,
         invariants: [boundInv, ...s.invariants.map(transformExpr)],
@@ -1682,7 +1765,7 @@ function transformStmt(s: TStmt, typeDecls: TypeDeclInfo[]): Stmt[] {
         const replaced = replacePathInTStmts(s.someBody, path, s.binder, s.binderTy);
         const someBody = transformStmts(replaced, typeDecls);
         const noneBody = transformStmts(s.noneBody, typeDecls);
-        const scrutinee: Expr | string = path.fields.length === 0 ? path.rootVar : transformExpr(s.scrutinee);
+        const scrutinee: Expr = path.fields.length === 0 ? varE(path.rootVar) : transformExpr(s.scrutinee);
         return [{
           kind: "match", scrutinee,
           arms: [
@@ -1720,7 +1803,7 @@ function mapStmtExprs(s: Stmt, r: (e: Expr) => Expr): Stmt {
 function buildMatchArms<T>(
   cases: { name: string; body: TStmt[] }[],
   varName: string | undefined, typeName: string | undefined, typeDecls: TypeDeclInfo[],
-  transformBody: (body: TStmt[], varName: string | undefined, fields: { name: string; tsType: string }[]) => T | null
+  transformBody: (body: TStmt[], varName: string | undefined, fields: { name: string; tsType: string }[], ctorName?: string) => T | null
 ): { pattern: MatchPattern; body: T }[] | null {
   const decl = typeName ? declOf(typeDecls, typeName) : undefined;
   const arms: { pattern: MatchPattern; body: T }[] = [];
@@ -1728,7 +1811,7 @@ function buildMatchArms<T>(
     const variant = decl?.variants?.find(v => v.name === c.name);
     const fields = variant?.fields ?? [];
     const pattern = buildMatchPattern(c.name, fields, varName);
-    const body = transformBody(c.body, varName, fields);
+    const body = transformBody(c.body, varName, fields, c.name);
     if (body === null) return null;
     arms.push({ pattern, body });
   }
@@ -1795,7 +1878,7 @@ function emitMatchStmt(
       arms.push({ pattern: pWild(), body: transformStmts(fallthrough, typeDecls) });
     }
   }
-  return { kind: "match", scrutinee: isPath ? transformExpr(scrutinee) : prefix, arms };
+  return { kind: "match", scrutinee: isPath ? transformExpr(scrutinee) : varE(prefix), arms };
 }
 
 /** Replace bare `var(oldName)` references → `var(newName)` with the given type.
@@ -1838,15 +1921,36 @@ function enumFieldSwitch(s: TStmt & { kind: "switch" }, typeDecls: TypeDeclInfo[
   };
 }
 
+/** Stamp variant ctor info onto datatype updates of the match scrutinee in
+ *  lowered arm bodies (`{ ...vn, f: v }`) — the statement-path twin of
+ *  `replaceFieldAccess`'s stamping. Emitters need the pin to use
+ *  per-constructor destructor names for collision-renamed fields. */
+function stampScrutineeUpdates(body: Stmt[], varName: string, ctorName: string, ctorOf: string): Stmt[] {
+  const stamp = (x: Expr): Expr | null => {
+    if (x.kind === "record" && !x.ctor && x.spread &&
+        x.spread.kind === "var" && x.spread.name === varName) {
+      return { ...x, ctor: ctorName, ctorOf,
+        fields: x.fields.map(f => ({ ...f, value: mapExpr(f.value, stamp) })) };
+    }
+    return null;
+  };
+  return body.map(st => mapStmt(st, stamp));
+}
+
 function emitSwitchStmt(s: TStmt & { kind: "switch" }, typeDecls: TypeDeclInfo[]): Stmt {
   const cases = s.cases.map(c => ({ name: c.label, body: c.body }));
   const ef = enumFieldSwitch(s, typeDecls);
+  const baseName = s.expr.ty.kind === "user" ? tyBaseName(s.expr.ty.name) : undefined;
   const arms = ef
     ? buildMatchArms(cases, undefined, ef.enumTyName, typeDecls, (body) => transformStmts(body, typeDecls))!
     : buildMatchArms(cases, s.expr.kind === "var" ? s.expr.name : "?", s.expr.ty.kind === "user" ? s.expr.ty.name : undefined, typeDecls,
-        (body, vn, fields) => transformStmts(replaceFieldAccessInTStmts(body, vn!, fields), typeDecls))!;
+        (body, vn, fields, ctorName) => {
+          let out = transformStmts(replaceFieldAccessInTStmts(body, vn!, fields), typeDecls);
+          if (ctorName && vn && baseName) out = stampScrutineeUpdates(out, vn, ctorName, baseName);
+          return out;
+        })!;
   if (s.defaultBody.length > 0) arms.push({ pattern: pWild(), body: transformStmts(s.defaultBody, typeDecls) });
-  return { kind: "match", scrutinee: ef ? ef.scrutinee : (s.expr.kind === "var" ? s.expr.name : "?"), arms };
+  return { kind: "match", scrutinee: ef ? ef.scrutinee : varE(s.expr.kind === "var" ? s.expr.name : "?"), arms };
 }
 
 /** Replace obj.field → replacement var in typed IR.
@@ -1986,7 +2090,7 @@ function transformPureBody(stmts: TStmt[], typeDecls: TypeDeclInfo[]): Expr | nu
           if (!someExpr) return null;
           const noneExpr = transformPureBody([...s.noneBody, ...rest], typeDecls);
           if (!noneExpr) return null;
-          const scrutinee: Expr | string = path.fields.length === 0 ? path.rootVar : transformExpr(s.scrutinee);
+          const scrutinee: Expr = path.fields.length === 0 ? varE(path.rootVar) : transformExpr(s.scrutinee);
           return {
             kind: "match", scrutinee,
             arms: [
@@ -2021,10 +2125,10 @@ function transformPureSwitch(s: TStmt & { kind: "switch" }, typeDecls: TypeDeclI
   const varName = s.expr.kind === "var" ? s.expr.name : undefined;
   const cases = s.cases.map(c => ({ name: c.label, body: c.body }));
   const arms = buildMatchArms(cases, varName, typeName, typeDecls,
-    (body, vn, fields) => {
+    (body, vn, fields, ctorName) => {
       let result = transformPureBody(body, typeDecls);
       if (!result) return null;
-      if (fields.length > 0 && vn) result = replaceFieldAccess(result, vn, fields);
+      if (fields.length > 0 && vn) result = replaceFieldAccess(result, vn, fields, ctorName, tyBaseName(typeName));
       return result;
     });
   if (!arms) return null;
@@ -2034,7 +2138,7 @@ function transformPureSwitch(s: TStmt & { kind: "switch" }, typeDecls: TypeDeclI
     arms.push({ pattern: pWild(), body });
   }
   if (s.expr.kind !== "var") return null;
-  return { kind: "match", scrutinee: s.expr.name, arms };
+  return { kind: "match", scrutinee: varE(s.expr.name), arms };
 }
 
 function transformPureMatch(chain: Chain, typeDecls: TypeDeclInfo[]): Expr | null {
@@ -2045,10 +2149,10 @@ function transformPureMatch(chain: Chain, typeDecls: TypeDeclInfo[]): Expr | nul
   // the statement-level counterpart of this substitution.
   const isSynthArrayUnion = decl?.discriminant === "__isArray__";
   const arms = buildMatchArms(cases, chain.varName, chain.typeName, typeDecls,
-    (body, vn, fields) => {
+    (body, vn, fields, ctorName) => {
       let result = transformPureBody(body, typeDecls);
       if (!result) return null;
-      if (fields.length > 0 && vn) result = replaceFieldAccess(result, vn, fields);
+      if (fields.length > 0 && vn) result = replaceFieldAccess(result, vn, fields, ctorName, tyBaseName(chain.typeName));
       if (isSynthArrayUnion && fields.length === 1 && vn) {
         result = replaceVarInExpr(result, vn, matchBinder(fields[0].name, vn));
       }
@@ -2065,7 +2169,7 @@ function transformPureMatch(chain: Chain, typeDecls: TypeDeclInfo[]): Expr | nul
       // Exactly one variant left — destructure for variant-specific field access.
       let body = transformPureBody(chain.fallthrough, typeDecls);
       if (!body) return null;
-      if (remaining.fields.length > 0) body = replaceFieldAccess(body, chain.varName, remaining.fields);
+      if (remaining.fields.length > 0) body = replaceFieldAccess(body, chain.varName, remaining.fields, remaining.name, tyBaseName(chain.typeName));
       if (isSynthArrayUnion && remaining.fields.length === 1) {
         body = replaceVarInExpr(body, chain.varName, matchBinder(remaining.fields[0].name, chain.varName));
       }
@@ -2076,7 +2180,7 @@ function transformPureMatch(chain: Chain, typeDecls: TypeDeclInfo[]): Expr | nul
       arms.push({ pattern: pWild(), body });
     }
   }
-  return { kind: "match", scrutinee: chain.varName, arms };
+  return { kind: "match", scrutinee: varE(chain.varName), arms };
 }
 
 // ── Generate type declarations ───────────────────────────────
@@ -2201,6 +2305,7 @@ export function transformModule(mod: TModule, specImport?: string, moduleBaseOve
   _forofCounters.clear();
   _liftCounter = 0;
   _typeDecls = mod.typeDecls;
+  _neededKindHelpers = new Map();
   _pureDefNames = new Set(mod.functions.filter(f => f.isPure).map(f => f.name));
   const typeDecls = mod.typeDecls.map(transformTypeDecl);
 
@@ -2273,28 +2378,6 @@ export function transformModule(mod: TModule, specImport?: string, moduleBaseOve
     };
   });
 
-  // Types file
-  const typesImports: string[] = ["LemmaScript"];
-  let typesFile: Module | null = null;
-  const pureNamespace: Decl[] = pureDefs.length > 0
-    ? [{ kind: "namespace", name: "Pure", decls: pureDefs }]
-    : [];
-  if (typeDecls.length > 0 || pureDefs.length > 0 || externDecls.length > 0) {
-    // Declaration order differs by backend. Dafny allows forward references, so
-    // externs go first to be in scope everywhere. Lean requires definition-before-use:
-    // an extern's signature may reference a declared type (e.g. `estimateTokens(m: AgentMessage)`),
-    // so types must precede externs, which in turn precede the pure mirrors that may call them.
-    const decls = _opts.backend === "lean"
-      ? [...typeDecls, ...externDecls, ...pureNamespace]
-      : [...externDecls, ...typeDecls, ...pureNamespace];
-    typesFile = {
-      comment: "  Generated by lsc — Lean types and pure function mirrors.",
-      imports: typesImports,
-      options: [],
-      decls,
-    };
-  }
-
   // Def file: Velvet methods
   // Pure functions get a thin wrapper that calls Pure.fnName
   // def-by-method functions also skip their method wrappers
@@ -2375,6 +2458,76 @@ export function transformModule(mod: TModule, specImport?: string, moduleBaseOve
     };
   });
 
+  // Types file — assembled after all body transforms, so needs discovered
+  // there (discriminator kind-helpers) are included.
+  const kindHelpers: Decl[] = [..._neededKindHelpers.values()].map(kindHelperDecl);
+
+  // ── Imported / undeclared user types: opaque by default ─────────────
+  // A module may reference types it imports (ir.ts uses typedir's `Ty`).
+  // Standalone compilation has no declaration for them; synthesize an
+  // opaque type — the value passes through, uninspectable, which is the
+  // only sound use of an undeclared type (same doctrine as _synthOpaque).
+  // Any attempted inspection still fails loudly: an opaque type has no
+  // constructors and no operations. Signature-level coverage (type-decl
+  // fields, params, returns, class fields, externs, consts); a body-level
+  // reference to an undeclared type still errors in the backend.
+  const referenced = new Set<string>();
+  const collectTy = (ty: Ty): void => {
+    switch (ty.kind) {
+      case "user": referenced.add(tyBaseName(ty.name)); return;
+      case "array": case "set": collectTy(ty.elem); return;
+      case "optional": collectTy(ty.inner); return;
+      case "map": collectTy(ty.key); collectTy(ty.value); return;
+      case "tuple": ty.elems.forEach(collectTy); return;
+      case "fn": ty.params.forEach(collectTy); collectTy(ty.result); return;
+      default: return;
+    }
+  };
+  const knownTypeNames = new Set<string>(typeDecls.map(d => (d as { name: string }).name));
+  const allTypeParams = new Set<string>();
+  // Exclude type params from the *source* decls — the transformed IR drops
+  // them for aliases (`type Step<S, A> = …`), and a generic alias's params
+  // must not be mistaken for imported types. Params may carry a `//@ type`
+  // decoration ("S(==)"); references collect as the bare name, so strip it.
+  const addTp = (tp: string): void => { allTypeParams.add(tp.replace(/\(.*$/, "").trim()); };
+  for (const d of mod.typeDecls) d.typeParams?.forEach(addTp);
+  for (const d of typeDecls) {
+    if (d.kind === "inductive") d.constructors.forEach(c => c.fields.forEach(f => collectTy(f.type)));
+    else if (d.kind === "structure") d.fields.forEach(f => collectTy(f.type));
+    else if (d.kind === "type-alias") collectTy(d.target);
+  }
+  for (const fn of mod.functions) { fn.typeParams.forEach(addTp); fn.params.forEach(p => collectTy(p.ty)); collectTy(fn.returnTy); }
+  for (const cls of mod.classes ?? []) {
+    cls.fields.forEach(f => collectTy(f.ty));
+    for (const m of cls.methods) { m.typeParams.forEach(addTp); m.params.forEach(p => collectTy(p.ty)); collectTy(m.returnTy); }
+  }
+  for (const ext of mod.externs ?? []) { ext.typeParams.forEach(addTp); ext.params.forEach(p => collectTy(p.ty)); collectTy(ext.returnTy); }
+  for (const c of mod.constants ?? []) collectTy(c.ty);
+  const opaqueImports: Decl[] = [...referenced]
+    .filter(n => !knownTypeNames.has(n) && !allTypeParams.has(n))
+    .map(n => ({ kind: "opaque-type" as const, name: n }));
+  const typesImports: string[] = ["LemmaScript"];
+  let typesFile: Module | null = null;
+  const pureNamespace: Decl[] = pureDefs.length > 0
+    ? [{ kind: "namespace", name: "Pure", decls: pureDefs }]
+    : [];
+  if (typeDecls.length > 0 || pureDefs.length > 0 || externDecls.length > 0 || opaqueImports.length > 0) {
+    // Declaration order differs by backend. Dafny allows forward references, so
+    // externs go first to be in scope everywhere. Lean requires definition-before-use:
+    // an extern's signature may reference a declared type (e.g. `estimateTokens(m: AgentMessage)`),
+    // so types must precede externs, which in turn precede the pure mirrors that may call them.
+    // Kind-helpers sit right after the datatypes they discriminate.
+    const decls = _opts.backend === "lean"
+      ? [...opaqueImports, ...typeDecls, ...kindHelpers, ...externDecls, ...pureNamespace]
+      : [...externDecls, ...opaqueImports, ...typeDecls, ...kindHelpers, ...pureNamespace];
+    typesFile = {
+      comment: "  Generated by lsc — Lean types and pure function mirrors.",
+      imports: typesImports,
+      options: [],
+      decls,
+    };
+  }
+
   const defImport = specImport ?? (typesFile ? `«${moduleBase}.types»` : null);
   const defBaseImports: string[] = defImport ? [defImport] : ["LemmaScript"];
   const defFile: Module = {
diff --git a/tools/src/typedir.ts b/tools/src/typedir.ts
index 994f65c..66c851c 100644
--- a/tools/src/typedir.ts
+++ b/tools/src/typedir.ts
@@ -92,7 +92,8 @@ export type TExpr =
       builtinId?: BuiltinId }
   | { kind: "index"; obj: TExpr; idx: TExpr; ty: Ty }
   | { kind: "field"; obj: TExpr; field: string; ty: Ty;
-      isDiscriminant?: boolean }            // true if this is a discriminant field access
+      isDiscriminant?: boolean;             // true if this is a discriminant field access
+      ofVariant?: string }                  // which union variant the field is read from, when narrowing determined it
   | { kind: "record"; spread: TExpr | null; fields: { name: string; value: TExpr }[]; ty: Ty }
   | { kind: "arrayLiteral"; elems: TExpr[]; ty: Ty }
   | { kind: "lambda"; params: { name: string; ty: Ty }[]; body: TStmt[]; ty: Ty }