diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index efcefd34b..30118bd36 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -809,15 +809,12 @@ jobs:
           - { os: macos-15, target: aarch64-apple-darwin }
           - { os: windows-2022, target: x86_64-pc-windows-msvc }
     runs-on: ${{ matrix.os }}
-    # The Intel macOS runner is the slowest host: 51 to 61 minutes for this job
-    # before certificates A and B were kernel data, and past 120 minutes (the
-    # limit it then had, cancelled) once the stress families of SP-02 and the
-    # 9000-arm match of SP-08 built them (the suite took 2.9 times as long on
-    # the arm Linux runner, 1064 to 3051 seconds). A leg cancelled at the limit
-    # says nothing about the code, and the only defence against it was to run
-    # the leg again. Twice the slowest observed time leaves the limit a bound on
-    # a hung job, not a race with the runner's speed.
-    timeout-minutes: 300
+    # The Intel macOS runner takes 51 to 61 minutes for this job, which is the
+    # limit it used to have: a leg cancelled at the limit says nothing about the
+    # code, and the only defence against it was to run the leg again. Twice the
+    # slowest observed time leaves the limit a bound on a hung job, not a race
+    # with the runner's speed.
+    timeout-minutes: 120
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
       - name: Install the pinned Rust toolchain
diff --git a/crates/lexlean/src/production/certificate.rs b/crates/lexlean/src/production/certificate.rs
index 02da2ccd9..186b6a287 100644
--- a/crates/lexlean/src/production/certificate.rs
+++ b/crates/lexlean/src/production/certificate.rs
@@ -428,16 +428,14 @@ fn record_source(
     kind: &str,
 ) -> Result<String, String> {
     let name = module.rsplit('.').next().unwrap_or(module);
-    let value = serde_json::to_value(data).map_err(|error| error.to_string())?;
-    crate::sdk::assemble(
+    crate::sdk::assemble_core(
         &crate::sdk::SourceHeader {
             name,
             glossaries: &[],
             imports: &[],
             title: &format!("Certificate {kind} {module}"),
         },
-        crate::sdk::ModuleKind::Core,
-        &value,
+        data,
     )
     .map_err(|error| error.message)
 }
diff --git a/crates/lexlean/src/production/certificate/data_a/boundary.rs b/crates/lexlean/src/production/certificate/data_a/boundary.rs
index 0f6769b29..cb6f3e964 100644
--- a/crates/lexlean/src/production/certificate/data_a/boundary.rs
+++ b/crates/lexlean/src/production/certificate/data_a/boundary.rs
@@ -1575,10 +1575,11 @@ impl<'a> Writer<'_, 'a> {
                 vars.push((parameter, encoded));
                 let binding = Binding { vars, pair: None };
                 let derived = self.chain_pf(&binding, inner, &arm.body, &checks, spec.direct)?;
+                let (_, pre_arms) = self.prepare_arms(arms)?;
                 let mut arms_pf =
-                    self.arm_hit(base, encoded, arms, arm_index, &fields, inner, derived)?;
+                    self.arm_hit(base, encoded, &pre_arms, arm_index, &fields, inner, derived)?;
                 for earlier in (0..arm_index).rev() {
-                    arms_pf = self.arm_miss(base, encoded, arms, earlier, arms_pf)?;
+                    arms_pf = self.arm_miss(base, encoded, &pre_arms, earlier, arms_pf)?;
                 }
                 let Expr::Var { name } = scrutinee else {
                     return Err(
diff --git a/crates/lexlean/src/production/certificate/data_a/matching.rs b/crates/lexlean/src/production/certificate/data_a/matching.rs
index aabd2594e..4a4160536 100644
--- a/crates/lexlean/src/production/certificate/data_a/matching.rs
+++ b/crates/lexlean/src/production/certificate/data_a/matching.rs
@@ -9,7 +9,56 @@ use crate::ir::semantic::{SemanticBranch, SemanticTerm, SemanticType, Step};
 use crate::production::kernel::{Given, Term};
 use crate::production::source::Constructor;
 
+/// The precomputed terms of one match arm, with the suffix of the arms after
+/// it.
+#[derive(Clone, Copy)]
+pub(super) struct PreArm {
+    shape: Term,
+    binders: Term,
+    body: Term,
+    rest: Term,
+}
+
 impl<'a> Writer<'_, 'a> {
+    /// Precompute the terms of each arm in `arms`, and the list of all arms
+    /// with the suffix after each position, right to left in $O(n)$.
+    pub(super) fn prepare_arms(&mut self, arms: &[Arm]) -> Result<(Term, Vec<PreArm>), String> {
+        let ty = self.ts("Arm");
+        let head = self.ts("Arm.arm");
+        let nil = self.b.konst0("List.nil");
+        let cons = self.b.konst0("List.cons");
+        let mut parts = Vec::with_capacity(arms.len());
+        let mut item_terms = Vec::with_capacity(arms.len());
+        for arm in arms {
+            let shape = self.shape_term(arm.shape);
+            let binders = self.numbers_term(&arm.binders);
+            let body = self.expr_term(&arm.body)?;
+            parts.push((shape, binders, body));
+            item_terms.push(self.b.apps(head, &[shape, binders, body]));
+        }
+        let mut list = self.b.app(nil, ty);
+        let mut pre = vec![
+            PreArm {
+                shape: 0,
+                binders: 0,
+                body: 0,
+                rest: 0,
+            };
+            arms.len()
+        ];
+        for index in (0..arms.len()).rev() {
+            let (shape, binders, body) = parts[index];
+            pre[index] = PreArm {
+                shape,
+                binders,
+                body,
+                rest: list,
+            };
+            list = self.b.apps(cons, &[ty, item_terms[index], list]);
+        }
+        Ok((list, pre))
+    }
+
     /// The derivation that the arm at `position` of `arms` is taken for the
     /// value `encoded`: the arm matches, binds `fields` over `env`, and its
     /// body is derived by `body`.
@@ -18,17 +67,13 @@ impl<'a> Writer<'_, 'a> {
         &mut self,
         env: Term,
         encoded: Term,
-        arms: &[Arm],
+        arms: &[PreArm],
         position: usize,
         fields: &[Term],
         extended: Term,
         body: Pf,
     ) -> Result<Pf, String> {
         let arm = arms.get(position).ok_or("a match lowered to fewer arms")?;
-        let shape = self.shape_term(arm.shape);
-        let binders = self.numbers_term(&arm.binders);
-        let body_expr = self.expr_term(&arm.body)?;
-        let rest = self.arms_list(&arms[position + 1..])?;
         let value_ty = self.value_ty();
         let list = self.b.list(value_ty, fields);
         let p = self.prog;
@@ -38,10 +83,10 @@ impl<'a> Writer<'_, 'a> {
                 ("p", p),
                 ("env", env),
                 ("v", encoded),
-                ("shape", shape),
-                ("binders", binders),
-                ("body", body_expr),
-                ("rest", rest),
+                ("shape", arm.shape),
+                ("binders", arm.binders),
+                ("body", arm.body),
+                ("rest", arm.rest),
                 ("fields", list),
                 ("env'", extended),
             ],
@@ -55,15 +100,11 @@ impl<'a> Writer<'_, 'a> {
         &mut self,
         env: Term,
         encoded: Term,
-        arms: &[Arm],
+        arms: &[PreArm],
         position: usize,
         later: Pf,
     ) -> Result<Pf, String> {
         let arm = arms.get(position).ok_or("a match lowered to fewer arms")?;
-        let shape = self.shape_term(arm.shape);
-        let binders = self.numbers_term(&arm.binders);
-        let body_expr = self.expr_term(&arm.body)?;
-        let rest = self.arms_list(&arms[position + 1..])?;
         let p = self.prog;
         self.apply(
             "convA_miss",
@@ -71,10 +112,10 @@ impl<'a> Writer<'_, 'a> {
                 ("p", p),
                 ("env", env),
                 ("v", encoded),
-                ("shape", shape),
-                ("binders", binders),
-                ("body", body_expr),
-                ("rest", rest),
+                ("shape", arm.shape),
+                ("binders", arm.binders),
+                ("body", arm.body),
+                ("rest", arm.rest),
             ],
             &[Given::Refl, Given::Proof(later.proof, later.ty)],
         )
@@ -184,6 +225,7 @@ impl<'a> Writer<'_, 'a> {
         let node = self.node_of(scope, whole);
         // Per constructor, in declaration order: the arm's width predicate,
         // value, and derivation, each abstracted over the arm's fields.
+        let (arms_term, pre_arms) = self.prepare_arms(arms)?;
         let mut fits_minors: Vec<(usize, Term)> = Vec::new();
         let mut value_minors: Vec<(usize, Term)> = Vec::new();
         let mut proof_minors: Vec<(usize, Term)> = Vec::new();
@@ -226,9 +268,9 @@ impl<'a> Writer<'_, 'a> {
                 self.constructor_value(&constructor, &scrutinee_ty, branch, &frees, scope)?;
             let encoded = self.b.app(scrutinee_enc, value);
             let mut proof =
-                self.arm_hit(env, encoded, arms, position, &fields, arm_env, body_pf)?;
+                self.arm_hit(env, encoded, &pre_arms, position, &fields, arm_env, body_pf)?;
             for earlier in (0..position).rev() {
-                proof = self.arm_miss(env, encoded, arms, earlier, proof)?;
+                proof = self.arm_miss(env, encoded, &pre_arms, earlier, proof)?;
             }
             let ctor_position = self.constructor_position(&constructor)?;
             let binders: Vec<(String, Term, Term)> = locals
@@ -315,7 +357,6 @@ impl<'a> Writer<'_, 'a> {
             .lam_over("__a", EXPLICIT, lean_scrutinee, bound, w_body);
         // ha : ∀ a, sv = a → ConvA p env (enc a) arms (Rel (G a) (W a)),
         // proved by cases on a with the arms' derivations as minors.
-        let arms_term = self.arms_list(arms)?;
         let encoded_bound = self.b.app(scrutinee_enc, bound);
         let g_a = self.b.app(g, bound);
         let w_a = self.b.app(w, bound);
@@ -445,8 +486,8 @@ impl<'a> Writer<'_, 'a> {
                 }
             }
         }
-        let arms_term = self.arms_list(arms)?;
-        let halves_term = self.arms_list(halves)?;
+        let (arms_term, pre_arms) = self.prepare_arms(arms)?;
+        let (halves_term, pre_halves) = self.prepare_arms(halves)?;
         // Per (first, second): the derivation of the program's arms, the
         // arm's predicate and its value.
         let mut proofs: Vec<[Term; 2]> = vec![[Term::default(); 2]; 2];
@@ -500,10 +541,11 @@ impl<'a> Writer<'_, 'a> {
             let fits = self.fits_of(body_pf)?;
             let value = self.src(&branch.body, &inner_scope)?;
             // The innermost Boolean, then the first, then the pair.
+            let (second_arms_term, pre_leaf_arms) = self.prepare_arms(leaf_arms)?;
             let leaf_hit = self.arm_hit(
                 pair_env,
                 second_encoded,
-                leaf_arms,
+                &pre_leaf_arms,
                 usize::from(second_value),
                 &[],
                 pair_env,
@@ -511,8 +553,13 @@ impl<'a> Writer<'_, 'a> {
             )?;
             let mut leaf_chain = leaf_hit;
             for earlier in (0..usize::from(second_value)).rev() {
-                leaf_chain =
-                    self.arm_miss(pair_env, second_encoded, leaf_arms, earlier, leaf_chain)?;
+                leaf_chain = self.arm_miss(
+                    pair_env,
+                    second_encoded,
+                    &pre_leaf_arms,
+                    earlier,
+                    leaf_chain,
+                )?;
             }
             let second_var_term = self.nat_u(second_var);
             let second_test = self.apply(
@@ -525,7 +572,6 @@ impl<'a> Writer<'_, 'a> {
                 ],
                 &[Given::Refl],
             )?;
-            let second_arms_term = self.arms_list(leaf_arms)?;
             let second_match_ty = self.ty_term(second_ty);
             let inner = self.apply(
                 "conv_match",
@@ -543,7 +589,7 @@ impl<'a> Writer<'_, 'a> {
             let half_hit = self.arm_hit(
                 pair_env,
                 first_encoded,
-                halves,
+                &pre_halves,
                 usize::from(first_value),
                 &[],
                 pair_env,
@@ -551,7 +597,8 @@ impl<'a> Writer<'_, 'a> {
             )?;
             let mut half_chain = half_hit;
             for earlier in (0..usize::from(first_value)).rev() {
-                half_chain = self.arm_miss(pair_env, first_encoded, halves, earlier, half_chain)?;
+                half_chain =
+                    self.arm_miss(pair_env, first_encoded, &pre_halves, earlier, half_chain)?;
             }
             let first_var_term = self.nat_u(first_var);
             let first_test = self.apply(
@@ -582,7 +629,7 @@ impl<'a> Writer<'_, 'a> {
             let top = self.arm_hit(
                 env,
                 encoded,
-                arms,
+                &pre_arms,
                 0,
                 &[first_encoded, second_encoded],
                 pair_env,
diff --git a/crates/lexlean/src/production/certificate/data_a/structural.rs b/crates/lexlean/src/production/certificate/data_a/structural.rs
index 2a8d4a14e..baa2ece6b 100644
--- a/crates/lexlean/src/production/certificate/data_a/structural.rs
+++ b/crates/lexlean/src/production/certificate/data_a/structural.rs
@@ -767,17 +767,18 @@ impl<'a> Writer<'_, 'a> {
             let enc = self.enc(&argument_ty)?;
             self.b.app(enc, constructed)
         };
+        let (arms_term, pre_arms) = self.prepare_arms(arms)?;
         let mut chain = self.arm_hit(
             env,
             scrutinee_encoded,
-            arms,
+            &pre_arms,
             branch_index,
             &arm_fields,
             arm_env,
             body_pf,
         )?;
         for earlier in (0..branch_index).rev() {
-            chain = self.arm_miss(env, scrutinee_encoded, arms, earlier, chain)?;
+            chain = self.arm_miss(env, scrutinee_encoded, &pre_arms, earlier, chain)?;
         }
         let p = self.prog;
         let number = match scrutinee_expr {
@@ -803,7 +804,6 @@ impl<'a> Writer<'_, 'a> {
             &[("p", p), ("env", env), ("x", x), ("v", scrutinee_encoded)],
             &[Given::Refl],
         )?;
-        let arms_term = self.arms_list(arms)?;
         let match_ty_term = self.ty_term(match_ty);
         let matched = self.apply(
             "conv_match",
diff --git a/crates/lexlean/src/production/certificate/data_b/align.rs b/crates/lexlean/src/production/certificate/data_b/align.rs
index aa0c45a05..6f501277e 100644
--- a/crates/lexlean/src/production/certificate/data_b/align.rs
+++ b/crates/lexlean/src/production/certificate/data_b/align.rs
@@ -2167,6 +2167,7 @@ impl<'g, 'a> Aligner<'g, 'a> {
         );
         let mut derivation = self.rule("mNil", g, fl, nil_jd, &[], &[])?;
         let mut indices = Vec::with_capacity(rarms.len());
+        let mut cursor = arms.len();
         for (pattern, block) in rarms.iter().rev() {
             self.refused()?;
             let (next, index, arm_term) = self.m_arm(
@@ -2175,6 +2176,7 @@ impl<'g, 'a> Aligner<'g, 'a> {
                 st,
                 view,
                 arms,
+                &mut cursor,
                 fm,
                 tau,
                 pattern,
@@ -2209,6 +2211,7 @@ impl<'g, 'a> Aligner<'g, 'a> {
         st: &Ty,
         view: bool,
         arms: &[Arm],
+        cursor: &mut usize,
         fm: bool,
         tau: &Ty,
         pattern: &Pat,
@@ -2220,9 +2223,11 @@ impl<'g, 'a> Aligner<'g, 'a> {
         let [st_term, view_term, arms_term, fm_term, tau_term] = fixed;
         let (idx_rest, rarms_rest) = suffix;
         let (shape, inner) = arm_outer(st, view, pattern)?;
-        let j = arms
+        let j = arms[..*cursor]
             .iter()
-            .position(|arm| arm.shape == shape)
+            .rposition(|arm| arm.shape == shape)
+            .inspect(|&found| *cursor = found)
+            .or_else(|| arms.iter().position(|arm| arm.shape == shape))
             .ok_or_else(|| format!("no arm has shape {shape:?}"))?;
         let arm = &arms[j];
         let types = self.checker.shape_fields(shape, st)?;
diff --git a/crates/lexlean/src/production/kernel.rs b/crates/lexlean/src/production/kernel.rs
index 6dd844533..cdcc76d13 100644
--- a/crates/lexlean/src/production/kernel.rs
+++ b/crates/lexlean/src/production/kernel.rs
@@ -64,6 +64,9 @@ pub struct Builder {
     /// The loose-variable bound of every node a walk has passed
     /// ([`Self::has_loose`]).
     loose: std::cell::RefCell<HashMap<Term, usize>>,
+    /// The least free-variable id (`$id`) reachable from each node, or
+    /// `usize::MAX` when the node mentions no free variable.
+    min_free: Vec<usize>,
 }
 
 /// The empty binder name, which the notation writes as `_`.
@@ -96,6 +99,67 @@ impl Builder {
             return index;
         }
         let index = self.nodes.len();
+        let (is_clean, loose_bound, min_free) = match &node {
+            CoreNode::BVar { i } => (true, Some(i + 1), usize::MAX),
+            CoreNode::Sort { .. } | CoreNode::Nat { .. } | CoreNode::String { .. } => {
+                (true, Some(0), usize::MAX)
+            }
+            CoreNode::Const { n, .. } => {
+                let free = n
+                    .strip_prefix("\u{1}free.")
+                    .and_then(|id| id.parse().ok())
+                    .unwrap_or(usize::MAX);
+                (!n.starts_with("\u{1}meta."), Some(0), free)
+            }
+            CoreNode::App { f, x } => {
+                let clean = self.clean.borrow();
+                let loose = self.loose.borrow();
+                (
+                    clean.contains(f) && clean.contains(x),
+                    loose.get(f).zip(loose.get(x)).map(|(&a, &b)| a.max(b)),
+                    self.min_free[*f].min(self.min_free[*x]),
+                )
+            }
+            CoreNode::Lambda { t, v, .. } | CoreNode::Forall { t, v, .. } => {
+                let clean = self.clean.borrow();
+                let loose = self.loose.borrow();
+                (
+                    clean.contains(t) && clean.contains(v),
+                    loose
+                        .get(t)
+                        .zip(loose.get(v))
+                        .map(|(&a, &b)| a.max(b.saturating_sub(1))),
+                    self.min_free[*t].min(self.min_free[*v]),
+                )
+            }
+            CoreNode::Let { t, v, body, .. } => {
+                let clean = self.clean.borrow();
+                let loose = self.loose.borrow();
+                (
+                    clean.contains(t) && clean.contains(v) && clean.contains(body),
+                    loose
+                        .get(t)
+                        .zip(loose.get(v))
+                        .zip(loose.get(body))
+                        .map(|((&a, &b), &c)| a.max(b).max(c.saturating_sub(1))),
+                    self.min_free[*t]
+                        .min(self.min_free[*v])
+                        .min(self.min_free[*body]),
+                )
+            }
+            CoreNode::Mdata { x, .. } | CoreNode::Projection { x, .. } => {
+                let clean = self.clean.borrow();
+                let loose = self.loose.borrow();
+                (clean.contains(x), loose.get(x).copied(), self.min_free[*x])
+            }
+        };
+        if is_clean {
+            self.clean.borrow_mut().insert(index);
+        }
+        if let Some(bound) = loose_bound {
+            self.loose.borrow_mut().insert(index, bound);
+        }
+        self.min_free.push(min_free);
         self.nodes.push(node.clone());
         self.shared.insert(node, index);
         index
@@ -262,6 +326,9 @@ impl Builder {
         if let Some(&done) = memo.get(&(term, cutoff)) {
             return done;
         }
+        if self.loose_bound(term) <= cutoff {
+            return term;
+        }
         let out = match self.nodes[term].clone() {
             CoreNode::BVar { i } => {
                 if i >= cutoff {
@@ -323,6 +390,9 @@ impl Builder {
     /// `body` with `#0` replaced by `arg` and every other loose variable
     /// lowered by one: the body of a binder instantiated at `arg`.
     pub fn instantiate(&mut self, body: Term, arg: Term) -> Term {
+        if self.loose_bound(body) == 0 {
+            return body;
+        }
         let mut memo = HashMap::new();
         self.instantiate_memo(body, arg, 0, &mut memo)
     }
@@ -337,6 +407,9 @@ impl Builder {
         if let Some(&done) = memo.get(&(term, depth)) {
             return done;
         }
+        if self.loose_bound(term) <= depth {
+            return term;
+        }
         let out = match self.nodes[term].clone() {
             CoreNode::BVar { i } => {
                 if i == depth {
diff --git a/crates/lexlean/src/production/kernel/ext.rs b/crates/lexlean/src/production/kernel/ext.rs
index 94c538333..9b0e39753 100644
--- a/crates/lexlean/src/production/kernel/ext.rs
+++ b/crates/lexlean/src/production/kernel/ext.rs
@@ -157,20 +157,28 @@ impl Builder {
 
     /// `term` with the free variable `free` bound by the binder around it.
     pub fn abstract_over(&mut self, term: Term, free: Term) -> Term {
+        let free_id = self.min_free[free];
+        if self.min_free[term] > free_id {
+            return term;
+        }
         let mut memo = HashMap::new();
-        self.abstract_memo(term, free, 0, &mut memo)
+        self.abstract_memo(term, free, free_id, 0, &mut memo)
     }
 
     fn abstract_memo(
         &mut self,
         term: Term,
         free: Term,
+        free_id: usize,
         depth: usize,
         memo: &mut HashMap<(Term, usize), Term>,
     ) -> Term {
         if term == free {
             return self.bvar(depth);
         }
+        if self.min_free[term] > free_id {
+            return term;
+        }
         if let Some(&done) = memo.get(&(term, depth)) {
             return done;
         }
@@ -181,32 +189,32 @@ impl Builder {
             | CoreNode::Nat { .. }
             | CoreNode::String { .. } => term,
             CoreNode::App { f, x } => {
-                let f = self.abstract_memo(f, free, depth, memo);
-                let x = self.abstract_memo(x, free, depth, memo);
+                let f = self.abstract_memo(f, free, free_id, depth, memo);
+                let x = self.abstract_memo(x, free, free_id, depth, memo);
                 self.app(f, x)
             }
             CoreNode::Lambda { n, b, t, v } => {
-                let t = self.abstract_memo(t, free, depth, memo);
-                let v = self.abstract_memo(v, free, depth + 1, memo);
+                let t = self.abstract_memo(t, free, free_id, depth, memo);
+                let v = self.abstract_memo(v, free, free_id, depth + 1, memo);
                 self.lam(&n, b, t, v)
             }
             CoreNode::Forall { n, b, t, v } => {
-                let t = self.abstract_memo(t, free, depth, memo);
-                let v = self.abstract_memo(v, free, depth + 1, memo);
+                let t = self.abstract_memo(t, free, free_id, depth, memo);
+                let v = self.abstract_memo(v, free, free_id, depth + 1, memo);
                 self.pi(&n, b, t, v)
             }
             CoreNode::Let { n, t, v, body, d } => {
-                let t = self.abstract_memo(t, free, depth, memo);
-                let v = self.abstract_memo(v, free, depth, memo);
-                let body = self.abstract_memo(body, free, depth + 1, memo);
+                let t = self.abstract_memo(t, free, free_id, depth, memo);
+                let v = self.abstract_memo(v, free, free_id, depth, memo);
+                let body = self.abstract_memo(body, free, free_id, depth + 1, memo);
                 self.let_node(&n, t, v, body, d)
             }
             CoreNode::Mdata { m, x } => {
-                let x = self.abstract_memo(x, free, depth, memo);
+                let x = self.abstract_memo(x, free, free_id, depth, memo);
                 self.mdata_node(m, x)
             }
             CoreNode::Projection { n, s, i, x } => {
-                let x = self.abstract_memo(x, free, depth, memo);
+                let x = self.abstract_memo(x, free, free_id, depth, memo);
                 self.projection(&n, &s, i, x)
             }
         };
@@ -348,19 +356,30 @@ impl Builder {
         if map.is_empty() {
             return term;
         }
+        let max_free = if from.iter().all(|&f| self.min_free[f] != usize::MAX) {
+            from.iter().map(|&f| self.min_free[f]).max()
+        } else {
+            None
+        };
         let mut memo = HashMap::new();
-        self.substitute_memo(term, &map, &mut memo)
+        self.substitute_memo(term, &map, max_free, &mut memo)
     }
 
     fn substitute_memo(
         &mut self,
         term: Term,
         map: &HashMap<Term, Term>,
+        max_free: Option<usize>,
         memo: &mut HashMap<Term, Term>,
     ) -> Term {
         if let Some(&replacement) = map.get(&term) {
             return replacement;
         }
+        if let Some(limit) = max_free {
+            if self.min_free[term] > limit {
+                return term;
+            }
+        }
         if let Some(&done) = memo.get(&term) {
             return done;
         }
@@ -371,32 +390,32 @@ impl Builder {
             | CoreNode::Nat { .. }
             | CoreNode::String { .. } => term,
             CoreNode::App { f, x } => {
-                let f = self.substitute_memo(f, map, memo);
-                let x = self.substitute_memo(x, map, memo);
+                let f = self.substitute_memo(f, map, max_free, memo);
+                let x = self.substitute_memo(x, map, max_free, memo);
                 self.app(f, x)
             }
             CoreNode::Lambda { n, b, t, v } => {
-                let t = self.substitute_memo(t, map, memo);
-                let v = self.substitute_memo(v, map, memo);
+                let t = self.substitute_memo(t, map, max_free, memo);
+                let v = self.substitute_memo(v, map, max_free, memo);
                 self.lam(&n, b, t, v)
             }
             CoreNode::Forall { n, b, t, v } => {
-                let t = self.substitute_memo(t, map, memo);
-                let v = self.substitute_memo(v, map, memo);
+                let t = self.substitute_memo(t, map, max_free, memo);
+                let v = self.substitute_memo(v, map, max_free, memo);
                 self.pi(&n, b, t, v)
             }
             CoreNode::Let { n, t, v, body, d } => {
-                let t = self.substitute_memo(t, map, memo);
-                let v = self.substitute_memo(v, map, memo);
-                let body = self.substitute_memo(body, map, memo);
+                let t = self.substitute_memo(t, map, max_free, memo);
+                let v = self.substitute_memo(v, map, max_free, memo);
+                let body = self.substitute_memo(body, map, max_free, memo);
                 self.let_node(&n, t, v, body, d)
             }
             CoreNode::Mdata { m, x } => {
-                let x = self.substitute_memo(x, map, memo);
+                let x = self.substitute_memo(x, map, max_free, memo);
                 self.mdata_node(m, x)
             }
             CoreNode::Projection { n, s, i, x } => {
-                let x = self.substitute_memo(x, map, memo);
+                let x = self.substitute_memo(x, map, max_free, memo);
                 self.projection(&n, &s, i, x)
             }
         };
@@ -534,8 +553,7 @@ impl Builder {
     /// Whether `term` mentions a free variable or a placeholder.
     #[must_use]
     pub fn has_placeholder(&self, term: Term) -> bool {
-        let mut seen = std::collections::HashSet::new();
-        self.placeholder_walk(term, &mut seen, true)
+        self.min_free[term] != usize::MAX || !self.meta_clean(term)
     }
 
     /// Whether `term` mentions a lemma's placeholder, a binder nothing solved.
@@ -601,40 +619,6 @@ impl Builder {
         status[&root]
     }
 
-    fn placeholder_walk(
-        &self,
-        term: Term,
-        seen: &mut std::collections::HashSet<Term>,
-        free_too: bool,
-    ) -> bool {
-        if !seen.insert(term) {
-            return false;
-        }
-        match &self.nodes[term] {
-            CoreNode::Const { n, .. } => n.starts_with(META) || (free_too && n.starts_with(FREE)),
-            CoreNode::BVar { .. }
-            | CoreNode::Sort { .. }
-            | CoreNode::Nat { .. }
-            | CoreNode::String { .. } => false,
-            CoreNode::App { f, x } => {
-                self.placeholder_walk(*f, seen, free_too)
-                    || self.placeholder_walk(*x, seen, free_too)
-            }
-            CoreNode::Lambda { t, v, .. } | CoreNode::Forall { t, v, .. } => {
-                self.placeholder_walk(*t, seen, free_too)
-                    || self.placeholder_walk(*v, seen, free_too)
-            }
-            CoreNode::Let { t, v, body, .. } => {
-                self.placeholder_walk(*t, seen, free_too)
-                    || self.placeholder_walk(*v, seen, free_too)
-                    || self.placeholder_walk(*body, seen, free_too)
-            }
-            CoreNode::Mdata { x, .. } | CoreNode::Projection { x, .. } => {
-                self.placeholder_walk(*x, seen, free_too)
-            }
-        }
-    }
-
     /// Assign the placeholders of `pattern` that `actual` has a term at, by
     /// comparing the two node by node. A shape the two do not share is left
     /// to the kernel.
@@ -699,6 +683,9 @@ impl Builder {
     /// binder: the type of `conv_cond` states `P b` and the type of the
     /// application states the predicate's body.
     pub fn instantiate_beta(&mut self, body: Term, arg: Term) -> Term {
+        if self.loose_bound(body) == 0 {
+            return body;
+        }
         let mut memo = HashMap::new();
         self.beta_memo(body, arg, 0, &mut memo)
     }
@@ -713,6 +700,9 @@ impl Builder {
         if let Some(&done) = memo.get(&(term, depth)) {
             return done;
         }
+        if self.loose_bound(term) <= depth {
+            return term;
+        }
         let out = match self.nodes[term].clone() {
             CoreNode::BVar { i } => {
                 if i == depth {
@@ -766,16 +756,16 @@ impl Builder {
 
     /// `term` with every solved placeholder replaced, transitively.
     fn resolve(&mut self, term: Term, solved: &HashMap<usize, Term>) -> Term {
-        let map: HashMap<String, Term> = solved
-            .iter()
-            .map(|(id, value)| (format!("{META}{id}"), *value))
-            .collect();
+        if solved.is_empty() || self.meta_clean(term) {
+            return term;
+        }
+        let values_clean = solved.values().all(|&value| self.meta_clean(value));
         let mut out = term;
         for _ in 0..64 {
             let mut memo = HashMap::new();
-            let next = self.resolve_memo(out, &map, &mut memo);
-            if next == out {
-                return out;
+            let next = self.resolve_memo(out, solved, &mut memo);
+            if values_clean || next == out {
+                return next;
             }
             out = next;
         }
@@ -787,7 +777,7 @@ impl Builder {
     fn resolve_memo(
         &mut self,
         term: Term,
-        map: &HashMap<String, Term>,
+        solved: &HashMap<usize, Term>,
         memo: &mut HashMap<Term, Term>,
     ) -> Term {
         if let Some(&done) = memo.get(&term) {
@@ -797,44 +787,46 @@ impl Builder {
             return term;
         }
         let out = match self.nodes[term].clone() {
-            CoreNode::Const { n, .. } => map.get(&n).copied().unwrap_or(term),
+            CoreNode::Const { .. } => self
+                .meta_id(term)
+                .and_then(|id| solved.get(&id).copied())
+                .unwrap_or(term),
             CoreNode::BVar { .. }
             | CoreNode::Sort { .. }
             | CoreNode::Nat { .. }
             | CoreNode::String { .. } => term,
             CoreNode::App { f, x } => {
                 let (head, _) = self.spine(f);
-                let replaced_head = self.meta_id(head).is_some()
-                    || matches!(&self.nodes[head], CoreNode::Const { n, .. } if map.contains_key(n));
-                let f2 = self.resolve_memo(f, map, memo);
-                let x2 = self.resolve_memo(x, map, memo);
+                let replaced_head = self.meta_id(head).is_some();
+                let f2 = self.resolve_memo(f, solved, memo);
+                let x2 = self.resolve_memo(x, solved, memo);
                 match self.nodes[f2].clone() {
                     CoreNode::Lambda { v, .. } if replaced_head => self.instantiate_beta(v, x2),
                     _ => self.app(f2, x2),
                 }
             }
             CoreNode::Lambda { n, b, t, v } => {
-                let t = self.resolve_memo(t, map, memo);
-                let v = self.resolve_memo(v, map, memo);
+                let t = self.resolve_memo(t, solved, memo);
+                let v = self.resolve_memo(v, solved, memo);
                 self.lam(&n, b, t, v)
             }
             CoreNode::Forall { n, b, t, v } => {
-                let t = self.resolve_memo(t, map, memo);
-                let v = self.resolve_memo(v, map, memo);
+                let t = self.resolve_memo(t, solved, memo);
+                let v = self.resolve_memo(v, solved, memo);
                 self.pi(&n, b, t, v)
             }
             CoreNode::Let { n, t, v, body, d } => {
-                let t = self.resolve_memo(t, map, memo);
-                let v = self.resolve_memo(v, map, memo);
-                let body = self.resolve_memo(body, map, memo);
+                let t = self.resolve_memo(t, solved, memo);
+                let v = self.resolve_memo(v, solved, memo);
+                let body = self.resolve_memo(body, solved, memo);
                 self.let_node(&n, t, v, body, d)
             }
             CoreNode::Mdata { m, x } => {
-                let x = self.resolve_memo(x, map, memo);
+                let x = self.resolve_memo(x, solved, memo);
                 self.mdata_node(m, x)
             }
             CoreNode::Projection { n, s, i, x } => {
-                let x = self.resolve_memo(x, map, memo);
+                let x = self.resolve_memo(x, solved, memo);
                 self.projection(&n, &s, i, x)
             }
         };
diff --git a/crates/lexlean/src/production/preserve.rs b/crates/lexlean/src/production/preserve.rs
index c032ec969..27240f2fb 100644
--- a/crates/lexlean/src/production/preserve.rs
+++ b/crates/lexlean/src/production/preserve.rs
@@ -224,11 +224,12 @@ pub struct CorrespondenceRules {
 pub fn correspondence_rules() -> Result<CorrespondenceRules, String> {
     const CORR: &str = "LexLeanPreservation.Rust.Corr";
     const SOUND: &str = "LexLeanPreservation.Rust.sound";
-    let load = |module: &str| -> Result<crate::ir::core::CoreModule, String> {
-        let path = native_source_path(module).ok_or_else(|| format!("no source for `{module}`"))?;
-        let source = embedded_text(&path).map_err(|diagnostic| diagnostic.message)?;
-        crate::ir::core::CoreModule::from_source(source, "1.2")
-            .map_err(|reason| format!("{path}: {reason}"))
+    let native = native().map_err(|diagnostic| diagnostic.message.clone())?;
+    let load = |module: &str| -> Result<&crate::ir::core::CoreModule, String> {
+        native
+            .modules
+            .get(module)
+            .ok_or_else(|| format!("the library has no module `{module}`"))
     };
     let corr = load("LexLeanPreservation.RustCorr")?;
     let constructors: Vec<String> = corr
diff --git a/crates/lexlean/src/sdk.rs b/crates/lexlean/src/sdk.rs
index 726bb2a6a..7a6170c29 100644
--- a/crates/lexlean/src/sdk.rs
+++ b/crates/lexlean/src/sdk.rs
@@ -322,6 +322,32 @@ pub fn assemble(
     Ok(out)
 }
 
+/// The whole `.lex.tex` source of a native core module, printed directly from
+/// its [`crate::ir::core::CoreModule`] without round-tripping through JSON.
+///
+/// # Errors
+///
+/// `data` that is not a well-formed core module of the current schema.
+pub(crate) fn assemble_core(
+    header: &SourceHeader<'_>,
+    data: &crate::ir::core::CoreModule,
+) -> Result<String, AuthoringError> {
+    let printed = crate::surface::core::print_module(data)
+        .map_err(|failure| error(format!("the module has no notation: {failure}"), None))?;
+    let mut out = format!("\\begin{{lexlean}}{{{}}}\n", header.name);
+    for glossary in header.glossaries {
+        out.push_str(&format!("\\useglossary{{{glossary}}}\n"));
+    }
+    for import in header.imports {
+        out.push_str(&format!("\\importmodule{{{import}}}\n"));
+    }
+    out.push_str(&format!(
+        "\\title{{{}}}\n\\begin{{{}}}\n{printed}\\end{{{}}}\n\\end{{lexlean}}\n",
+        header.title, CORE.environment, CORE.environment
+    ));
+    Ok(out)
+}
+
 #[cfg(test)]
 mod tests {
     use serde_json::json;