diff --git a/egglog-experimental/dd/src/interpret.rs b/egglog-experimental/dd/src/interpret.rs
index 00831dda..bca4fe74 100644
--- a/egglog-experimental/dd/src/interpret.rs
+++ b/egglog-experimental/dd/src/interpret.rs
@@ -690,11 +690,18 @@ fn view_column_read_apply(
         .get(&op.view_name)
         .ok_or_else(|| anyhow!("view-column read view `{}` is not registered", op.view_name))?;
     let keys = &args[..op.n_keys];
-    let fallback = args[op.n_keys];
-    Ok(match lookup_existing(eg, view, keys, index) {
-        Some(values) => Value::new(values[op.col_idx]),
-        None => fallback,
-    })
+    match lookup_existing(eg, view, keys, index) {
+        Some(values) => Ok(Value::new(values[op.col_idx])),
+        None if op.has_fallback => Ok(args[op.n_keys]),
+        // A fallback-free lookup halts the rule on the reference backend. This
+        // interpreter has no way to abandon one action mid-flight, so report it
+        // instead of inventing a value; callers only use it where another table
+        // already witnesses the row.
+        None => Err(anyhow!(
+            "view-column lookup on `{}` found no row for its key",
+            op.view_name
+        )),
+    }
 }
 
 #[cfg(test)]
diff --git a/egglog-experimental/dd/src/lib.rs b/egglog-experimental/dd/src/lib.rs
index d91c7d07..994bf3f1 100644
--- a/egglog-experimental/dd/src/lib.rs
+++ b/egglog-experimental/dd/src/lib.rs
@@ -197,6 +197,10 @@ pub(crate) struct ViewOp {
     pub(crate) out_arity: usize,
     /// Output column to read (view-column read only).
     pub(crate) col_idx: usize,
+    /// Whether the reader takes a trailing fallback argument used when the key is
+    /// absent. A fallback-free reader has no answer for an absent key, so the DD
+    /// path reports it rather than inventing one.
+    pub(crate) has_fallback: bool,
 }
 
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
@@ -232,6 +236,34 @@ impl Default for EGraph {
 }
 
 impl EGraph {
+    /// Register a view-column reader the DD interpreter intercepts (the db-path
+    /// external function only panics). `has_fallback` selects the reader's
+    /// absent-key behavior; see [`ViewOp::has_fallback`].
+    fn register_view_column_op(
+        &mut self,
+        view_name: String,
+        n_keys: usize,
+        col_idx: usize,
+        has_fallback: bool,
+    ) -> ExternalFunctionId {
+        let id = Backend::new_panic(
+            self,
+            format!("view-column read for `{view_name}` reached the db path; DD must intercept it"),
+        );
+        self.view_column_read_ops.insert(
+            id,
+            ViewOp {
+                view_name,
+                n_keys,
+                // A view-column reader never inserts, so out_arity is unused.
+                out_arity: 0,
+                col_idx,
+                has_fallback,
+            },
+        );
+        id
+    }
+
     /// Construct a fresh Differential Dataflow backend. Rule bodies run on the
     /// in-process DD join; body primitives and head actions are applied
     /// host-side into the mirror. Pass this backend to
@@ -1042,11 +1074,14 @@ impl<'a> MergeTransaction<'a> {
         let view = self.view_op_table(op)?;
         let n_keys = op.n_keys;
         let key: Row = args[..n_keys].into();
-        let fallback = args[n_keys];
-        Ok(match self.current_row(view, n_keys, &key) {
-            Some(current) => current.values[op.col_idx],
-            None => fallback,
-        })
+        match self.current_row(view, n_keys, &key) {
+            Some(current) => Ok(current.values[op.col_idx]),
+            None if op.has_fallback => Ok(args[n_keys]),
+            None => Err(anyhow!(
+                "view-column lookup on `{}` found no row for its key",
+                op.view_name
+            )),
+        }
     }
 
     fn view_op_table(&self, op: &ViewOp) -> Result<FunctionId> {
@@ -2620,6 +2655,7 @@ impl Backend for EGraph {
                 n_keys,
                 out_arity,
                 col_idx: 0,
+                has_fallback: false,
             },
         );
         id
@@ -2631,21 +2667,16 @@ impl Backend for EGraph {
         n_keys: usize,
         col_idx: usize,
     ) -> ExternalFunctionId {
-        let id = Backend::new_panic(
-            self,
-            format!("view-column read for `{view_name}` reached the db path; DD must intercept it"),
-        );
-        self.view_column_read_ops.insert(
-            id,
-            ViewOp {
-                view_name,
-                n_keys,
-                // A view-column reader never inserts, so out_arity is unused.
-                out_arity: 0,
-                col_idx,
-            },
-        );
-        id
+        self.register_view_column_op(view_name, n_keys, col_idx, true)
+    }
+
+    fn register_view_column_lookup(
+        &mut self,
+        view_name: String,
+        n_keys: usize,
+        col_idx: usize,
+    ) -> ExternalFunctionId {
+        self.register_view_column_op(view_name, n_keys, col_idx, false)
     }
 
     // -- capability flags ---------------------------------------------------
diff --git a/egglog/CHANGELOG.md b/egglog/CHANGELOG.md
index 24dddf61..430f9541 100644
--- a/egglog/CHANGELOG.md
+++ b/egglog/CHANGELOG.md
@@ -2,6 +2,8 @@
 
 ## [Unreleased] - ReleaseDate
 
+- In the term/proof encoding, drive a view's eq-sort child rebuild from a `UF` edge instead of from the view. Each view gets one hidden `:merge` term→row index per distinct child eq-sort, and each indexed child position gets a rule joining a `UF` edge against that index — mirroring how a native rebuild iterates the e-nodes referencing a changed e-class rather than matching the view. The index entry already binds the row's key, so the row's value tuple is read on the rule's right-hand side rather than joined in its body.
+- New backend SPI `Backend::register_view_column_lookup`: a fallback-free `(keys) -> column` read of an FD view. An absent key returns no value, which halts the calling rule — letting a rule read a row another table already witnesses without inventing a value when it is missing.
 - Add a `(begin <action>*)` command and a `(let <var> (begin <action>* <expr>))` form that run a block of actions once, immediately, with a shared *local* scope (`let`s bind local variables, not global functions); `let`-begin additionally binds the global `<var>` to the block's trailing value. In the term/proof encoding, each top-level action's minted temporaries — and the shared `let`s introduced by the common-subexpression prepass — now run inside one such block instead of as separate top-level `let`s, so a temporary no longer becomes its own global function/table. This removes the per-proof-node table blow-up that made building a large static graph under the encoding slow (dominant cost on graphs with many top-level terms). A *user-written* `begin` block is reported unsupported under the term/proof encoding for now (proof checking models top-level actions individually, so a block's local bindings have no checkable representation); the encoding's own generated blocks are unaffected.
 - Common-subexpression prepass for the term/proof encoding (`ast::cse`, run over the program before encoding): within an action scope, a constructor application occurring more than once is bound to a shared `let` and its occurrences rewritten to that variable, so it is interned once. A top-level action that gains shared `let`s becomes a `begin` block, so they stay local rather than adding a global table per hoisted subterm.
 - In the term/proof encoding, when a `union` operand is a freshly-built constructor term, build it directly into the other operand's e-class instead of minting a fresh id and unioning it away: a plain view `set` points the constructor's children at the other operand's (target) e-class, and the view's congruence `:merge` handles the case where the term already exists. This reuses ids and drops the corresponding `@UF` rows (union-heavy workloads run substantially faster and use less memory in both term and proof mode). In proof mode the view row carries the equality proof `target = f(children)`, composed from the union's rule justification and a `Congr` chain over canonicalized children, with the built-in operand's term kept on its own id so proof reconstruction stays unambiguous.
diff --git a/egglog/egglog-backend-trait/src/backend_impl.rs b/egglog/egglog-backend-trait/src/backend_impl.rs
index 8e1fe862..b1e16c5e 100644
--- a/egglog/egglog-backend-trait/src/backend_impl.rs
+++ b/egglog/egglog-backend-trait/src/backend_impl.rs
@@ -252,6 +252,15 @@ impl Backend for EGraph {
         EGraph::register_view_column_read(self, view_name, n_keys, col_idx)
     }
 
+    fn register_view_column_lookup(
+        &mut self,
+        view_name: String,
+        n_keys: usize,
+        col_idx: usize,
+    ) -> ExternalFunctionId {
+        EGraph::register_view_column_lookup(self, view_name, n_keys, col_idx)
+    }
+
     fn set_report_level(&mut self, level: ReportLevel) {
         EGraph::set_report_level(self, level);
     }
diff --git a/egglog/egglog-backend-trait/src/lib.rs b/egglog/egglog-backend-trait/src/lib.rs
index c5d7bb50..b4eb8036 100644
--- a/egglog/egglog-backend-trait/src/lib.rs
+++ b/egglog/egglog-backend-trait/src/lib.rs
@@ -427,6 +427,22 @@ pub trait Backend: Send + Sync {
         ))
     }
 
+    /// Like [`Backend::register_view_column_read`], but with no fallback:
+    /// `(keys) -> column`, and an absent key halts the rule that called it. Lets a
+    /// rule read a row it has already established exists — via another table that
+    /// tracks the view — without joining the view itself, and without inventing a
+    /// value for a row that is not there. The default registers a panic.
+    fn register_view_column_lookup(
+        &mut self,
+        view_name: String,
+        _n_keys: usize,
+        _col_idx: usize,
+    ) -> ExternalFunctionId {
+        self.new_panic(format!(
+            "this backend does not support view-column lookups for view `{view_name}`"
+        ))
+    }
+
     // -- diagnostics --------------------------------------------------------
 
     /// Set the verbosity of the per-iteration timing report.
diff --git a/egglog/egglog-bridge/src/lib.rs b/egglog/egglog-bridge/src/lib.rs
index 31542e5c..e0b6df1d 100644
--- a/egglog/egglog-bridge/src/lib.rs
+++ b/egglog/egglog-bridge/src/lib.rs
@@ -384,6 +384,26 @@ impl EGraph {
         )))
     }
 
+    /// Fallback-free view-column read: `(keys) -> column`. Returning `None` on an
+    /// absent key halts the calling rule, so a caller that cannot name a
+    /// meaningful default simply does nothing for that row.
+    pub fn register_view_column_lookup(
+        &mut self,
+        view_name: String,
+        n_keys: usize,
+        col_idx: usize,
+    ) -> ExternalFunctionId {
+        let registry = self.action_registry.clone();
+        self.register_external_func(Box::new(make_external_func(
+            move |state: &mut ExecutionState, args: &[Value]| {
+                let registry = registry.read().unwrap();
+                let action = registry.lookup_table(&view_name)?.clone();
+                let vals = action.lookup_values(state, &args[..n_keys])?;
+                Some(vals[col_idx])
+            },
+        )))
+    }
+
     pub fn free_external_func(&mut self, func: ExternalFunctionId) {
         // A cached panic with more than one reference is kept alive (just
         // decrement); one at its last reference — or any func that is not a
diff --git a/egglog/src/proofs/proof_encoding.md b/egglog/src/proofs/proof_encoding.md
index 8a09329a..0041a7d5 100644
--- a/egglog/src/proofs/proof_encoding.md
+++ b/egglog/src/proofs/proof_encoding.md
@@ -486,13 +486,50 @@ with the leader (the view's `:merge` keeps the smaller).
         :ruleset rebuilding :name "rebuild_rule" :internal-include-subsumed)
 ```
 
-A rule for an **eq-sort child** instead re-keys the row: it `set`s the view at the
-canonicalized children and deletes the stale row (proof mode composes a `Congr` at
-that child index). Because `UF_<Sort>` has no row for a canonical term
-(identity-on-miss), a column already at its leader simply does not match, so no
-self-loops or default lookups are needed. Subsumption markers
-(`to_subsume_<Constructor>`) are likewise re-keyed to their leaders so a subsumed
-row stays subsumed after its children move.
+A rule for an **eq-sort child** is driven by a `UF_<Sort>` edge rather than by
+matching the view. Each view gets one hidden *rebuild index* per distinct child
+eq-sort,
+
+```text
+(function MulIndex_Math (Math Math Math) Unit :merge old :internal-hidden :unextractable)
+```
+
+holding, for every view row, one entry per `Math` child: that child first, then
+the row's whole key. Leading with the child makes "which rows mention this term"
+a key-prefix lookup — the same access pattern a native rebuild uses when it walks
+the e-nodes referencing a changed e-class. One rule per indexed child position
+joins a `UF_Math` edge against the index; here, position 0 of `Mul`:
+
+```text
+(rule ((= (values leader plf) (UF_Math follower))
+       (!= follower leader)
+       (MulIndex_Math follower follower c1))
+      ((let e (view-col0-MulView follower c1))
+       (set (MulView leader c1) (values e ()))
+       (set (MulIndex_Math leader leader c1) ())
+       (set (MulIndex_Math c1 leader c1) ())
+       (delete (MulView follower c1))
+       (delete (MulIndex_Math follower follower c1))
+       (delete (MulIndex_Math c1 follower c1)))
+        :ruleset rebuilding :unsafe-seminaive :name "rebuild_rule" :internal-include-subsumed)
+```
+
+The moved term is bound at a known position, so its leader is a plain
+substitution and proof mode composes a single `Congr` at that position from
+`plf`, the edge proof the body already bound.
+
+The index entry also binds the row's key, so the row's value tuple is read in the
+*action* (`view-col<i>-<View>`) instead of joining the view as a third body atom.
+Those readers take no fallback: an absent key halts the rule, exactly as a failing
+body join would. Reading the view in the action is what makes the rule
+`:unsafe-seminaive`.
+
+The index is maintained wherever a view row is written or deleted, so it tracks
+the view exactly. Container children are not indexed — they have no `UF_<Sort>`
+row to drive a lookup — and keep the per-column `:naive` rule below. Subsumption
+markers (`to_subsume_<Constructor>`) are re-keyed to their leaders by their own
+per-column rules, so a subsumed row stays subsumed after its children move;
+subsuming a view row keeps it, so it leaves the index untouched.
 
 # Globals
 
diff --git a/egglog/src/proofs/proof_encoding.rs b/egglog/src/proofs/proof_encoding.rs
index e6c6b0d5..1ddd15e4 100644
--- a/egglog/src/proofs/proof_encoding.rs
+++ b/egglog/src/proofs/proof_encoding.rs
@@ -98,6 +98,19 @@ enum CarriedProofs {
     EclassToTerm,
 }
 
+/// A materialized rebuild index on one function's view, covering the view's key
+/// columns of a single eq-sort. The table is `(term, <all key columns>) -> Unit`
+/// and holds one row per indexed key column, with that column's term leading.
+/// `positions` are those key-column indices. Leading with the term makes "which
+/// rows mention this term" a key-prefix lookup, which is how the `@UF`-driven
+/// rebuild rule finds the rows it must re-canonicalize.
+#[derive(Clone)]
+pub(crate) struct ViewIndex {
+    pub name: String,
+    pub sort_name: String,
+    pub positions: Vec<usize>,
+}
+
 // TODO refactor so that encoding state is optional on the e-graph, ProofNames not optional on EncodingState. Then we don't have to clone proof names everywhere.
 #[derive(Clone)]
 pub(crate) struct EncodingState {
@@ -117,6 +130,9 @@ pub(crate) struct EncodingState {
     /// Maps container sort name -> the name of its registered proof-producing
     /// container-rebuild primitive (`ContainerRebuildProof`). Proof mode only.
     pub container_rebuild_proof_name: HashMap<String, String>,
+    /// Function name -> the materialized rebuild indexes on its view, one per
+    /// distinct eq-sort among the view's key columns (see [`ViewIndex`]).
+    pub view_index: HashMap<String, Vec<ViewIndex>>,
     pub term_header_added: bool,
     // TODO this is very ugly- we should separate out a typechecking struct
     // since we didn't need an entire e-graph
@@ -141,6 +157,7 @@ impl EncodingState {
             proof_func_parent: HashMap::default(),
             container_rebuild_name: HashMap::default(),
             container_rebuild_proof_name: HashMap::default(),
+            view_index: HashMap::default(),
             term_header_added: false,
             original_typechecking: None,
             proofs_enabled: false,
@@ -513,7 +530,6 @@ impl<'a> ProofInstrumentor<'a> {
         let proof_sort = self.proof_sort();
         let trans = self.proof_names().eq_trans_constructor.clone();
         let sym = self.proof_names().eq_sym_constructor.clone();
-        let view = self.view_name(&ctor_name);
         let (dedup_args, fv_nat, nat_prf, nat_to_dedup) = self.build_natural_with_congr(
             res,
             &ctor_name,
@@ -539,10 +555,7 @@ impl<'a> ProofInstrumentor<'a> {
         // the target. Emitting `(F dedup_args target)` would add the guest's
         // shape to `target`'s term relation, making `target`'s `@Ast` ambiguous
         // during proof reconstruction (which reads term rows, not views).
-        let dedup_disp = ListDisplay(&dedup_args, " ").to_string();
-        res.push(format!(
-            "(set ({view} {dedup_disp}) (values {target} {view_proof}))"
-        ));
+        res.push(self.update_fd_view(&ctor_name, &dedup_args, target, &view_proof));
         res.push(format!("(let {guest} {target})"));
         let sv = self.mint(res, &sym, &view_proof, &proof_sort);
         let guest_conn = self.mint(res, &trans, &format!("{nat_to_dedup} {sv}"), &proof_sort);
@@ -758,6 +771,9 @@ impl<'a> ProofInstrumentor<'a> {
         let view_name = self.view_name(&fdecl.name);
         let in_sorts = ListDisplay(schema.input.clone(), " ");
         let fresh_sort = self.egraph.parser.symbol_gen.fresh("view");
+        // Register the rebuild indexes before instrumenting any view write for
+        // this function, so every write site can emit its index maintenance.
+        let index_decls = self.declare_view_indexes(fdecl);
         let delete_rule = self.delete_and_subsume(fdecl);
         let to_delete_name = self.delete_name(&fdecl.name);
         let subsumed_name = self.subsumed_name(&fdecl.name);
@@ -880,6 +896,7 @@ impl<'a> ProofInstrumentor<'a> {
             {view_decl}
             (function {to_delete_name} ({in_sorts}) Unit :no-merge :internal-hidden)
             (function {subsumed_name} ({in_sorts}) Unit :no-merge :internal-hidden)
+            {index_decls}
             {delete_rule}",
         ))
     }
@@ -1098,8 +1115,9 @@ impl<'a> ProofInstrumentor<'a> {
     }
 
     /// Write a row into a functional-dependency view
-    /// `(set (@FView children) (values eclass proof))`. Re-setting an existing `children` key with a
-    /// different `eclass` triggers the view's `:merge`.
+    /// `(set (@FView children) (values eclass proof))`, plus the row's rebuild-index
+    /// entries. Re-setting an existing `children` key with a different `eclass`
+    /// triggers the view's `:merge`.
     pub(super) fn update_fd_view(
         &mut self,
         fname: &str,
@@ -1108,12 +1126,115 @@ impl<'a> ProofInstrumentor<'a> {
         proof: &str,
     ) -> String {
         let view_name = self.view_name(fname);
+        let index_inserts = self.view_index_inserts(fname, children);
         format!(
-            "(set ({view_name} {}) (values {value} {proof}))",
+            "(set ({view_name} {}) (values {value} {proof}))\n{index_inserts}",
             ListDisplay(children, " ")
         )
     }
 
+    /// Declare one materialized rebuild index per distinct eq-sort among a view's
+    /// key columns, record them in [`EncodingState::view_index`], and return the
+    /// declarations. Container key columns get none: they carry no `@UF` row to
+    /// drive a lookup and are canonicalized structurally instead.
+    ///
+    /// Must run before any view write for this function is instrumented, so the
+    /// metadata is present when [`Self::view_index_inserts`] /
+    /// [`Self::view_index_deletes`] are consulted.
+    fn declare_view_indexes(&mut self, fdecl: &ResolvedFunctionDecl) -> String {
+        let types = fdecl.resolved_schema.view_types();
+        let n_keys = types.len() - 1;
+        let key_sorts = types[..n_keys]
+            .iter()
+            .map(|t| t.name().to_string())
+            .collect::<Vec<_>>()
+            .join(" ");
+        let mut by_sort: Vec<(String, Vec<usize>)> = Vec::new();
+        for i in Self::view_index_positions(&types, n_keys) {
+            let sort = types[i].name().to_string();
+            match by_sort.iter_mut().find(|(s, _)| *s == sort) {
+                Some((_, positions)) => positions.push(i),
+                None => by_sort.push((sort, vec![i])),
+            }
+        }
+        let mut decls = String::new();
+        let mut entries = Vec::new();
+        for (sort_name, positions) in by_sort {
+            let index_name = self
+                .egraph
+                .parser
+                .symbol_gen
+                .fresh(&format!("{}Index_{sort_name}", fdecl.name));
+            decls.push_str(&format!(
+                "(function {index_name} ({sort_name} {key_sorts}) Unit :merge old :internal-hidden :unextractable)\n"
+            ));
+            entries.push(ViewIndex {
+                name: index_name,
+                sort_name,
+                positions,
+            });
+        }
+        self.egraph
+            .proof_state
+            .view_index
+            .insert(fdecl.name.clone(), entries);
+        decls
+    }
+
+    /// The view key positions that get a rebuild index: the non-container
+    /// eq-sort ones. Every such position is indexed, including the first, since
+    /// the rebuild rule is driven by an `@UF` delta on any child.
+    fn view_index_positions(types: &[ArcSort], n_keys: usize) -> Vec<usize> {
+        (0..n_keys)
+            .filter(|&i| !types[i].is_eq_container_sort() && types[i].is_eq_sort())
+            .collect()
+    }
+
+    /// [`Self::view_index_inserts`], appended to `res` only when the view has
+    /// indexes (so a view with no eq-sort children emits no blank statement).
+    fn push_view_index_inserts(&mut self, res: &mut Stmts, fname: &str, key: &[String]) {
+        let inserts = self.view_index_inserts(fname, key);
+        if !inserts.is_empty() {
+            res.push(inserts);
+        }
+    }
+
+    /// Insert a view row into each of its rebuild indexes: one entry per indexed
+    /// key column, `(set (<index> key[pos] <whole key>) ())`. `key` is the view's
+    /// key columns (the children).
+    pub(super) fn view_index_inserts(&mut self, fname: &str, key: &[String]) -> String {
+        self.view_index_ops(fname, key, |name, term, whole| {
+            format!("(set ({name} {term} {whole}) ())")
+        })
+    }
+
+    /// Remove a view row from each of its rebuild indexes, mirroring
+    /// [`Self::view_index_inserts`]. Emitted wherever a view row is deleted.
+    pub(super) fn view_index_deletes(&mut self, fname: &str, key: &[String]) -> String {
+        self.view_index_ops(fname, key, |name, term, whole| {
+            format!("(delete ({name} {term} {whole}))")
+        })
+    }
+
+    fn view_index_ops(
+        &mut self,
+        fname: &str,
+        key: &[String],
+        op: impl Fn(&str, &str, &str) -> String,
+    ) -> String {
+        let Some(indexes) = self.egraph.proof_state.view_index.get(fname).cloned() else {
+            return String::new();
+        };
+        let whole = format!("{}", ListDisplay(key, " "));
+        let mut out = Vec::new();
+        for vi in &indexes {
+            for &pos in &vi.positions {
+                out.push(op(&vi.name, &key[pos], &whole));
+            }
+        }
+        out.join("\n")
+    }
+
     /// Intern the term/proof/AST/proof-list node `{name}(args_joined)` and return
     /// its id. Every such node table is hash-consed (see [`Self::hash_cons`]), so
     /// building the same node twice reuses one id instead of piling up
@@ -1285,6 +1406,8 @@ impl<'a> ProofInstrumentor<'a> {
             "(let {canon} ({set_if_empty} {} {fv} ()))",
             ListDisplay(args, " ")
         ));
+        // `set-if-empty` writes the view row itself, so index its key here.
+        self.push_view_index_inserts(res, &func_type.name, args);
         canon
     }
 
@@ -1384,13 +1507,16 @@ impl<'a> ProofInstrumentor<'a> {
         let dedup = self.fresh_var();
         let vprf = self.fresh_var();
         let view_proof = crate::proofs::proof_fresh::view_proof_prim_name(&view);
-        let dedup_args = ListDisplay(&dedup_args, " ");
         res.push(format!(
             "(set ({term_proof_constructor} {fv_nat}) {nat_prf})"
         ));
         res.push(format!(
-            "(let {dedup} ({set_if_empty} {dedup_args} {fv_nat} {nat_to_dedup_term}))"
+            "(let {dedup} ({set_if_empty} {} {fv_nat} {nat_to_dedup_term}))",
+            ListDisplay(&dedup_args, " ")
         ));
+        // `set-if-empty` writes the view row itself, so index its key here.
+        self.push_view_index_inserts(res, &func_type.name, &dedup_args);
+        let dedup_args = ListDisplay(&dedup_args, " ");
         res.push(format!(
             "(let {vprf} ({view_proof} {dedup_args} {nat_to_dedup_term}))"
         ));
diff --git a/egglog/src/proofs/proof_encoding_rebuild.rs b/egglog/src/proofs/proof_encoding_rebuild.rs
index 61af67b9..9a381f1c 100644
--- a/egglog/src/proofs/proof_encoding_rebuild.rs
+++ b/egglog/src/proofs/proof_encoding_rebuild.rs
@@ -3,10 +3,29 @@
 //! that execute requested deletes/subsumptions. (`@UF` path compression stays
 //! in [`super::proof_encoding`].)
 
-use super::proof_encoding::{ProofInstrumentor, Stmts};
+use super::proof_encoding::{ProofInstrumentor, Stmts, ViewIndex};
 use crate::typechecking::FuncType;
 use crate::*;
 
+/// How a maintenance-rebuild rule is evaluated.
+///
+/// `EncodingState::force_proof_naive` does not apply to these rules. It swaps an
+/// RHS-reading rule for a `:naive` equivalent so tests can compare the two, which
+/// only holds for a rule that does not write the tables its own body joins. A
+/// rebuild rule re-keys the very view and index rows it matches, so its `:naive`
+/// form stops after one pass per match instead of iterating that feedback to a
+/// fixpoint, and the two forms saturate at different databases.
+enum RebuildEval {
+    /// The rule's body sees every atom it depends on.
+    Seminaive,
+    /// A primitive in the rule reads `@UF` tables the body does not join on, and
+    /// no delta on them drives the rule.
+    Naive,
+    /// A primitive in the rule's *action* reads `@UF`, but the body joins the
+    /// driving `@UF` delta, which makes that read sound.
+    UnsafeSeminaive,
+}
+
 /// Which FD-view value column [`ProofInstrumentor::fd_value_rebuild_rule`] rebuilds.
 enum ValueRebuild {
     /// The value is the term's e-class (constructors and globals).
@@ -22,14 +41,10 @@ enum ValueRebuild {
 impl ProofInstrumentor<'_> {
     /// Rules that execute deletion and subsumption based on the tables requesting the deletion/subsumption.
     pub(super) fn delete_and_subsume(&mut self, fdecl: &ResolvedFunctionDecl) -> String {
-        let child_names = fdecl
-            .schema
-            .input
-            .iter()
-            .enumerate()
-            .map(|(i, _)| format!("c{i}_"))
-            .collect::<Vec<_>>()
-            .join(" ");
+        let child_vars: Vec<String> = (0..fdecl.schema.input.len())
+            .map(|i| format!("c{i}_"))
+            .collect();
+        let child_names = child_vars.join(" ");
         let to_delete_name = self.delete_name(&fdecl.name);
         let subsumed_name = self.subsumed_name(&fdecl.name);
         let view_name = self.view_name(&fdecl.name);
@@ -38,17 +53,19 @@ impl ProofInstrumentor<'_> {
 
         // The view is keyed by children only, so match its value tuple to
         // delete/subsume by key (the bridge re-reads every value column when
-        // subsuming a tuple-output view). Deletion removes the row by key;
-        // subsumption marks it subsumed (kept for size/proofs but excluded from
-        // matching).
+        // subsuming a tuple-output view). Deletion removes the row by key, taking
+        // its rebuild-index entries with it; subsumption keeps the row (excluded
+        // from matching but retained for size/proofs), so the index is untouched.
         let e = self.fresh_var();
         let pf = self.fresh_var();
         let e2 = self.fresh_var();
         let pf2 = self.fresh_var();
+        let index_deletes = self.view_index_deletes(&fdecl.name, &child_vars);
         format!(
             "(rule (({to_delete_name} {child_names})
                     (= (values {e} {pf}) ({view_name} {child_names})))
                    ((delete ({view_name} {child_names}))
+                    {index_deletes}
                     (delete ({to_delete_name} {child_names})))
                     :ruleset {delete_subsume_ruleset}
                     :name \"{fresh_name}\")
@@ -62,29 +79,36 @@ impl ProofInstrumentor<'_> {
 
     /// Wrap one maintenance-rebuild rule (`facts` -> `actions`) with the rebuilding
     /// ruleset, a fresh name, and `:internal-include-subsumed` (so stale rows are
-    /// rebuilt too). `naive` marks rules whose primitives read `@UF` tables the rule
-    /// body doesn't join on.
-    fn rebuild_rule(&mut self, facts: &str, actions: &str, naive: bool) -> String {
+    /// rebuilt too).
+    fn rebuild_rule(&mut self, facts: &str, actions: &str, eval: RebuildEval) -> String {
         let ruleset = self.proof_names().rebuilding_ruleset_name.clone();
         let fresh_name = self.egraph.parser.symbol_gen.fresh("rebuild_rule");
-        let naive = if naive { ":naive " } else { "" };
+        let eval = match eval {
+            RebuildEval::Seminaive => "",
+            RebuildEval::Naive => ":naive ",
+            RebuildEval::UnsafeSeminaive => ":unsafe-seminaive ",
+        };
         format!(
-            "(rule ({facts})\n     ({actions})\n     :ruleset {ruleset} {naive}:name \"{fresh_name}\" :internal-include-subsumed)\n"
+            "(rule ({facts})\n     ({actions})\n     :ruleset {ruleset} {eval}:name \"{fresh_name}\" :internal-include-subsumed)\n"
         )
     }
 
-    /// Rebuild rules that keep a view canonical: one rule per rebuildable child
-    /// column (a canonical column has no `@UF` row, so the rule simply doesn't
-    /// match), plus a rule for the FD view's value column. A stale eq-sort column is
-    /// replaced by its `@UF` leader, a stale container by its rebuilt value.
+    /// Rebuild rules that keep a view canonical, plus a rule for the FD view's
+    /// value column.
+    ///
+    /// The view's eq-sort children are canonicalized by one rule per distinct
+    /// child eq-sort ([`Self::eq_sort_rebuild_rule`]), driven by an `@UF` delta
+    /// joined against that sort's rebuild index. Container children keep a
+    /// per-column `:naive` rule ([`Self::container_child_rebuild_rule`]): a
+    /// container has no `@UF` row to drive a rule, and its rebuild primitive
+    /// reads `@UF` tables the body does not join on. The value column is
+    /// canonicalized by [`Self::fd_value_rebuild_rule`].
     ///
     /// A child update re-keys the row (`set` at the canonicalized children, then
-    /// `delete`); a collision on the new key runs the view's `:merge`. The value
-    /// column is canonicalized by [`Self::fd_value_rebuild_rule`]. In proof mode
-    /// each rule composes the updated view proof, and a container update records the
-    /// rebuilt container's `<CSort>Proof`.
+    /// `delete`, index entries following the row); a collision on the new key runs
+    /// the view's `:merge`. In proof mode each rule composes the updated view
+    /// proof, and a container update records the rebuilt container's `<CSort>Proof`.
     pub(super) fn rebuilding_rules(&mut self, fdecl: &ResolvedFunctionDecl) -> Vec<Command> {
-        let proofs = self.proofs_enabled();
         // A global's output *is* its e-class (like a constructor's), so it takes the
         // e-class rebuild below (union-tracking) — not the custom-output rebuild
         // (congruence), which would emit a nonsensical `Congr` on its nullary term.
@@ -95,93 +119,24 @@ impl ProofInstrumentor<'_> {
         // Key columns of the view row: the children (the value tuple is unkeyed).
         let n_keys = n - 1;
         let key_vars: Vec<String> = (0..n_keys).map(child).collect();
-        let view_name = self.view_name(&fdecl.name);
-        let keys_str = format!("{}", ListDisplay(&key_vars, " "));
 
         let mut rules = String::new();
-        // One rule per rebuildable key column (re-keys the row via set + delete).
         for (i, ty) in types[..n_keys].iter().enumerate() {
-            let is_container = ty.is_eq_container_sort();
-            if !is_container && !ty.is_eq_sort() {
-                continue;
+            if ty.is_eq_container_sort() {
+                rules.push_str(&self.container_child_rebuild_rule(fdecl, &key_vars, i, ty));
+            }
+        }
+        let indexes = self
+            .egraph
+            .proof_state
+            .view_index
+            .get(&fdecl.name)
+            .cloned()
+            .unwrap_or_default();
+        for vi in &indexes {
+            for pos in vi.positions.clone() {
+                rules.push_str(&self.eq_sort_rebuild_rule(fdecl, &key_vars, vi, pos));
             }
-            let ci = child(i);
-            let canon = format!("c{i}_canon_");
-            let (query_view, value_var, view_prf) = self.query_fd_view(&fdecl.name, &key_vars);
-            // Canonicalize the column with the container rebuild primitive or a `@UF`
-            // lookup, and build the proof pieces. Container-reading rules are `:naive`
-            // (the primitive reads `@UF` tables the rule doesn't join on).
-            let (canon_fact, proof_lets, pf_arg, cproof_set) = if is_container {
-                let value_prim = self.container_rebuild_prim(ty);
-                let canon_fact = format!("(= {canon} ({value_prim} {ci}))");
-                if proofs {
-                    let congr = self.proof_names().congr_constructor.clone();
-                    let trans = self.proof_names().eq_trans_constructor.clone();
-                    let sym = self.proof_names().eq_sym_constructor.clone();
-                    let proof_sort = self.proof_sort();
-                    let proof_prim = self.container_rebuild_proof_prim(ty);
-                    let rebuild_pf = self.fresh_var();
-                    let cproof = self.term_proof_name(ty.name());
-                    // proof_lets: bind the container rebuild proof, then mint the congr proof.
-                    let mut lets = Stmts::new();
-                    lets.push(format!("(let {rebuild_pf} ({proof_prim} {ci}))"));
-                    let new_pf = self.mint(
-                        &mut lets,
-                        &congr,
-                        &format!("{view_prf} {i} {rebuild_pf}"),
-                        &proof_sort,
-                    );
-                    // cproof_set: mint (Sym rebuild_pf), (Trans .. rebuild_pf), then record it.
-                    let mut cproof_stmts = Stmts::new();
-                    let sym_pf = self.mint(&mut cproof_stmts, &sym, &rebuild_pf, &proof_sort);
-                    let trans_pf = self.mint(
-                        &mut cproof_stmts,
-                        &trans,
-                        &format!("{sym_pf} {rebuild_pf}"),
-                        &proof_sort,
-                    );
-                    cproof_stmts.push(format!("(set ({cproof} {canon}) {trans_pf})"));
-                    (
-                        canon_fact,
-                        lets.join("\n                             "),
-                        new_pf,
-                        cproof_stmts.join("\n                             "),
-                    )
-                } else {
-                    (canon_fact, String::new(), "()".to_string(), String::new())
-                }
-            } else {
-                let uf_name = self.uf_name(ty.name());
-                let uf_prf = self.fresh_var();
-                let canon_fact = format!("(= (values {canon} {uf_prf}) ({uf_name} {ci}))");
-                if proofs {
-                    let congr = self.proof_names().congr_constructor.clone();
-                    let proof_sort = self.proof_sort();
-                    let mut lets = Stmts::new();
-                    let new_pf = self.mint(
-                        &mut lets,
-                        &congr,
-                        &format!("{view_prf} {i} {uf_prf}"),
-                        &proof_sort,
-                    );
-                    (
-                        canon_fact,
-                        lets.join("\n                             "),
-                        new_pf,
-                        String::new(),
-                    )
-                } else {
-                    (canon_fact, String::new(), "()".to_string(), String::new())
-                }
-            };
-            let mut updated = key_vars.clone();
-            updated[i] = canon.clone();
-            let updated_view = self.update_fd_view(&fdecl.name, &updated, &value_var, &pf_arg);
-            let facts = format!("{query_view}\n{canon_fact}\n(!= {ci} {canon})");
-            let actions = format!(
-                "{proof_lets}\n{updated_view}\n{cproof_set}\n(delete ({view_name} {keys_str}))"
-            );
-            rules.push_str(&self.rebuild_rule(&facts, &actions, is_container));
         }
         // FD view value column (see [`Self::fd_value_rebuild_rule`]). A
         // constructor/global's value *is* its e-class; a custom function's
@@ -207,6 +162,141 @@ impl ProofInstrumentor<'_> {
         self.parse_program(&rules)
     }
 
+    /// The `:naive` per-column rebuild for a container child at key position `i`:
+    /// rebuild the container with its primitive, then re-key the row (`set` at the
+    /// rebuilt children, `delete` the old key) and move the row's index entries
+    /// with it. In proof mode the row proof gains a `Congr` at position `i` and
+    /// the rebuilt container gets its reflexive `<CSort>Proof` anchor.
+    fn container_child_rebuild_rule(
+        &mut self,
+        fdecl: &ResolvedFunctionDecl,
+        key_vars: &[String],
+        i: usize,
+        ty: &ArcSort,
+    ) -> String {
+        let view_name = self.view_name(&fdecl.name);
+        let keys_str = format!("{}", ListDisplay(key_vars, " "));
+        let index_deletes = self.view_index_deletes(&fdecl.name, key_vars);
+        let ci = &key_vars[i];
+        let canon = format!("c{i}_canon_");
+        let (query_view, value_var, view_prf) = self.query_fd_view(&fdecl.name, key_vars);
+        let value_prim = self.container_rebuild_prim(ty);
+        let canon_fact = format!("(= {canon} ({value_prim} {ci}))");
+        let (proof_lets, pf_arg, cproof_set) = if self.proofs_enabled() {
+            let congr = self.proof_names().congr_constructor.clone();
+            let trans = self.proof_names().eq_trans_constructor.clone();
+            let sym = self.proof_names().eq_sym_constructor.clone();
+            let proof_sort = self.proof_sort();
+            let proof_prim = self.container_rebuild_proof_prim(ty);
+            let rebuild_pf = self.fresh_var();
+            let cproof = self.term_proof_name(ty.name());
+            // proof_lets: bind the container rebuild proof, then mint the congr proof.
+            let mut lets = Stmts::new();
+            lets.push(format!("(let {rebuild_pf} ({proof_prim} {ci}))"));
+            let new_pf = self.mint(
+                &mut lets,
+                &congr,
+                &format!("{view_prf} {i} {rebuild_pf}"),
+                &proof_sort,
+            );
+            // cproof_set: mint (Sym rebuild_pf), (Trans .. rebuild_pf), then record it.
+            let mut cproof_stmts = Stmts::new();
+            let sym_pf = self.mint(&mut cproof_stmts, &sym, &rebuild_pf, &proof_sort);
+            let trans_pf = self.mint(
+                &mut cproof_stmts,
+                &trans,
+                &format!("{sym_pf} {rebuild_pf}"),
+                &proof_sort,
+            );
+            cproof_stmts.push(format!("(set ({cproof} {canon}) {trans_pf})"));
+            (
+                lets.join("\n                      "),
+                new_pf,
+                cproof_stmts.join("\n                      "),
+            )
+        } else {
+            (String::new(), "()".to_string(), String::new())
+        };
+        let mut updated = key_vars.to_vec();
+        updated[i] = canon.clone();
+        let updated_view = self.update_fd_view(&fdecl.name, &updated, &value_var, &pf_arg);
+        let facts = format!("{query_view}\n{canon_fact}\n(!= {ci} {canon})");
+        let actions = format!(
+            "{proof_lets}\n{updated_view}\n{cproof_set}\n(delete ({view_name} {keys_str}))\n{index_deletes}"
+        );
+        self.rebuild_rule(&facts, &actions, RebuildEval::Naive)
+    }
+
+    /// The rebuild rule for eq-sort child position `pos`, reached through `vi`'s
+    /// index.
+    ///
+    /// An `@UF_<S>` edge on some term is joined against the index to find the rows
+    /// holding that term at `pos` — a key-prefix lookup, the same access pattern a
+    /// native rebuild uses when it walks the e-nodes referencing a changed
+    /// e-class, rather than matching the view once per row. Binding the moved term
+    /// at a known position makes its leader a static substitution, so the action
+    /// re-keys the row and (proof mode) composes one `@Congr` at `pos` from the
+    /// edge proof the body already bound — no per-child union-find reads and no
+    /// reflexive steps for children that did not move.
+    ///
+    /// The row's value tuple is read in the action rather than joined in the body:
+    /// the index entry already binds the key, and the reads are fallback-free, so
+    /// a row that is gone halts the rule exactly as a failing body join would.
+    fn eq_sort_rebuild_rule(
+        &mut self,
+        fdecl: &ResolvedFunctionDecl,
+        key_vars: &[String],
+        vi: &ViewIndex,
+        pos: usize,
+    ) -> String {
+        let proofs = self.proofs_enabled();
+        let view_name = self.view_name(&fdecl.name);
+        let uf_name = self.uf_name(&vi.sort_name);
+
+        // The moved term occupies key position `pos`, so it is the same variable in
+        // the `@UF` edge and in the index entry.
+        let follower = self.fresh_var();
+        let leader = self.fresh_var();
+        let leader_pf = self.fresh_var();
+        let mut keys = key_vars.to_vec();
+        keys[pos] = follower.clone();
+        let keys_str = format!("{}", ListDisplay(&keys, " "));
+        let index_deletes = self.view_index_deletes(&fdecl.name, &keys);
+        let uf_atom = format!("(= (values {leader} {leader_pf}) ({uf_name} {follower}))");
+        let index_atom = format!("({} {follower} {keys_str})", vi.name);
+
+        let value_var = self.fresh_var();
+        let view_prf = self.fresh_var();
+        let mut actions = Stmts::new();
+        let col = |i| crate::proofs::proof_fresh::view_col_prim_name(&view_name, i);
+        actions.push(format!("(let {value_var} ({} {keys_str}))", col(0)));
+        let pf_arg = if proofs {
+            actions.push(format!("(let {view_prf} ({} {keys_str}))", col(1)));
+            let congr = self.proof_names().congr_constructor.clone();
+            let proof_sort = self.proof_sort();
+            self.mint(
+                &mut actions,
+                &congr,
+                &format!("{view_prf} {pos} {leader_pf}"),
+                &proof_sort,
+            )
+        } else {
+            "()".to_string()
+        };
+        let mut updated = keys.clone();
+        updated[pos] = leader.clone();
+        actions.push(self.update_fd_view(&fdecl.name, &updated, &value_var, &pf_arg));
+        actions.push(format!("(delete ({view_name} {keys_str}))"));
+        actions.push(index_deletes);
+
+        let facts = format!("{uf_atom}\n(!= {follower} {leader})\n{index_atom}");
+        self.rebuild_rule(
+            &facts,
+            &actions.join("\n                      "),
+            RebuildEval::UnsafeSeminaive,
+        )
+    }
+
     /// One rule that canonicalizes an FD view's stale value column.
     ///
     /// * [`ValueRebuild::Eclass`] (constructors/globals): the value *is* the
@@ -278,7 +368,7 @@ impl ProofInstrumentor<'_> {
         let facts = format!(
             "{query_view}\n(= (values {canon} {uf_prf}) ({value_uf_name} {value_var}))\n(!= {value_var} {canon})"
         );
-        self.rebuild_rule(&facts, &actions, false)
+        self.rebuild_rule(&facts, &actions, RebuildEval::Seminaive)
     }
 
     /// The [`ValueRebuild::ContainerOutput`] arm of
@@ -337,7 +427,7 @@ impl ProofInstrumentor<'_> {
         let facts = format!("{query_view}\n{canon_fact}\n(!= {value_var} {canon})");
         let actions =
             format!("{proof_lets}\n(delete ({view_name} {keys_str}))\n{set_canon}\n{cproof_set}");
-        self.rebuild_rule(&facts, &actions, true)
+        self.rebuild_rule(&facts, &actions, RebuildEval::Naive)
     }
 
     /// Rules that update the to_subsume tables when children change. One rule per
diff --git a/egglog/src/proofs/proof_fresh.rs b/egglog/src/proofs/proof_fresh.rs
index 7bc9d9a5..e9729691 100644
--- a/egglog/src/proofs/proof_fresh.rs
+++ b/egglog/src/proofs/proof_fresh.rs
@@ -34,6 +34,13 @@ pub(crate) fn view_proof_prim_name(view_name: &str) -> String {
     format!("view-proof-{view_name}")
 }
 
+/// Deterministic name of an FD view's fallback-free reader for output column
+/// `col`: `(keys) -> column`, halting the calling rule when the key is absent.
+/// See [`set_if_empty_prim_name`] for why the prefix carries no internal marker.
+pub(crate) fn view_col_prim_name(view_name: &str, col: usize) -> String {
+    format!("view-col{col}-{view_name}")
+}
+
 /// Register an FD view's `set-if-empty` primitive and (in proof mode) its
 /// proof-column reader, so the encoding can canonicalize a freshly-built term
 /// to the view's canonical e-class at insertion time. `out_sorts` is the view's
@@ -65,7 +72,7 @@ pub(crate) fn register_set_if_empty(
     if out_sorts.len() >= 2 {
         let view_proof = ViewProof {
             name: view_proof_prim_name(view_name),
-            key_sorts,
+            key_sorts: key_sorts.clone(),
             proof_sort: out_sorts[1].clone(),
         };
         let name = view_name.to_string();
@@ -77,6 +84,42 @@ pub(crate) fn register_set_if_empty(
             move |backend, _| backend.register_view_column_read(name.clone(), n_keys, 1),
         );
     }
+
+    // Fallback-free readers, one per output column, for a rule that has already
+    // established the row exists and only needs its values (see
+    // `Backend::register_view_column_lookup`).
+    for (col, out) in out_sorts.iter().enumerate() {
+        let view_col = ViewCol {
+            name: view_col_prim_name(view_name, col),
+            key_sorts: key_sorts.clone(),
+            out_sort: out.clone(),
+        };
+        let name = view_name.to_string();
+        eg.add_backend_op_primitive(view_col, WriteState::valid_contexts(), move |backend, _| {
+            backend.register_view_column_lookup(name.clone(), n_keys, col)
+        });
+    }
+}
+
+/// Reads one output column of an FD view by key, with no fallback: an absent key
+/// halts the calling rule (see [`view_col_prim_name`]).
+#[derive(Clone)]
+struct ViewCol {
+    name: String,
+    key_sorts: Vec<ArcSort>,
+    out_sort: ArcSort,
+}
+
+impl Primitive for ViewCol {
+    fn name(&self) -> &str {
+        &self.name
+    }
+    fn get_type_constraints(&self, span: &Span) -> Box<dyn TypeConstraint> {
+        // (keys…) -> column
+        let mut sig = self.key_sorts.clone();
+        sig.push(self.out_sort.clone());
+        SimpleTypeConstraint::new(&self.name, sig, span.clone()).into_box()
+    }
 }
 
 /// `set-if-empty`: get-or-insert-with-default on an FD view. Looks up
diff --git a/egglog/src/proofs/proof_tests.rs b/egglog/src/proofs/proof_tests.rs
index bce43ac5..a372d729 100644
--- a/egglog/src/proofs/proof_tests.rs
+++ b/egglog/src/proofs/proof_tests.rs
@@ -71,6 +71,71 @@ mod tests {
         }
     }
 
+    /// Every view row must carry its rebuild-index entries. The single
+    /// `@UF`-driven rebuild rule reaches the rows mentioning a term only through
+    /// that index, so a row missing its entries is never re-canonicalized and
+    /// silently stays stale.
+    #[test]
+    fn rebuild_index_covers_every_view_row() {
+        use crate::util::HashSet;
+        use egglog_backend_trait::BackendExt;
+
+        let files = [
+            "tests/calc.egg",
+            "tests/integer_math.egg",
+            "tests/web-demo/eqsat-basic.egg",
+            "tests/web-demo/unification-points-to.egg",
+        ];
+
+        for file in files {
+            let source = std::fs::read_to_string(file)
+                .unwrap_or_else(|e| panic!("couldn't read {file}: {e}"));
+            let mut egraph = crate::EGraph::new_with_proofs();
+            egraph
+                .parse_and_run_program(Some(file.to_string()), &source)
+                .unwrap_or_else(|e| panic!("{file} failed: {e}"));
+
+            let view_index = egraph.proof_state.view_index.clone();
+            for (fname, indexes) in &view_index {
+                let Some(view_name) = egraph.proof_state.proof_names.view_name.get(fname) else {
+                    continue;
+                };
+                let Some(view) = egraph.functions.get(view_name) else {
+                    continue;
+                };
+                let (view_id, n_keys) = (view.backend_id, view.schema.input.len());
+                let mut keys = Vec::new();
+                egraph.backend.for_each_while(view_id, |row| {
+                    keys.push(row.vals[..n_keys].to_vec());
+                    true
+                });
+
+                for vi in indexes {
+                    let Some(index) = egraph.functions.get(&vi.name) else {
+                        continue;
+                    };
+                    let mut entries = HashSet::default();
+                    egraph.backend.for_each_while(index.backend_id, |row| {
+                        entries.insert(row.vals[..n_keys + 1].to_vec());
+                        true
+                    });
+                    for key in &keys {
+                        for &pos in &vi.positions {
+                            let mut want = vec![key[pos]];
+                            want.extend_from_slice(key);
+                            assert!(
+                                entries.contains(&want),
+                                "{file}: {} row {key:?} is missing its {} entry at position {pos}",
+                                view_name,
+                                vi.name,
+                            );
+                        }
+                    }
+                }
+            }
+        }
+    }
+
     /// A user rule marked `:naive` must stay `:naive` through proof encoding;
     /// dropping it would silently switch the rule to seminaive evaluation.
     #[test]
diff --git a/egglog/tests/snapshots/files__proofs__array_proof_testing.snap b/egglog/tests/snapshots/files__proofs__array_proof_testing.snap
index 01ffa3fe..e82d28f3 100644
--- a/egglog/tests/snapshots/files__proofs__array_proof_testing.snap
+++ b/egglog/tests/snapshots/files__proofs__array_proof_testing.snap
@@ -1,6 +1,5 @@
 ---
 source: egglog/tests/files.rs
-assertion_line: 279
 expression: proof_snapshot
 ---
 (let t0 (select (store (AVar "mem1") (Var "r1") (Num 42)) (Var "r1")))
diff --git a/egglog/tests/snapshots/files__proofs__combinators_proof_testing.snap b/egglog/tests/snapshots/files__proofs__combinators_proof_testing.snap
index eaa5de35..327e7679 100644
--- a/egglog/tests/snapshots/files__proofs__combinators_proof_testing.snap
+++ b/egglog/tests/snapshots/files__proofs__combinators_proof_testing.snap
@@ -1,6 +1,5 @@
 ---
 source: egglog/tests/files.rs
-assertion_line: 279
 expression: proof_snapshot
 ---
 (let t0 (If (Var "x") (N 0) (N 1)))
diff --git a/egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap b/egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap
index 569927db..c3a89f99 100644
--- a/egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap
+++ b/egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap
@@ -9,7 +9,7 @@ expression: proof_snapshot
   (= (@ExistsConstructor) (@ExistsConstructor))
   (name "@prove_exists_rule")
   (premises prf0 (Fiat (= (Z) (Z))) prf0 (Eval) (Fiat (= t1 t1)))
-  (substitution (@v117 (Z)) (@v116 (S (Z))) (@v119 t0) (@v118 (S (Z)))))
+  (substitution (@v121 t0) (@v119 (Z)) (@v118 (S (Z))) (@v120 (S (Z)))))
 (let t0 (pair (Z) (S (Z))))
 (let t1 (HasPair t0))
 (Rule
@@ -20,7 +20,7 @@ expression: proof_snapshot
     (Fiat (= (S (Z)) (S (Z))))
     (Eval)
     (Fiat (= t1 t1)))
-  (substitution (@v278 t0) (@v276 (Z)) (@v277 (S (Z)))))
+  (substitution (@v278 (Z)) (@v279 (S (Z))) (@v280 t0)))
 (let t0 (vec-of (Z) (S (Z))))
 (let t1 (HasVec t0))
 (Rule
@@ -31,7 +31,7 @@ expression: proof_snapshot
     (Fiat (= (S (Z)) (S (Z))))
     (Eval)
     (Fiat (= t1 t1)))
-  (substitution (@v422 (Z)) (@v424 t0) (@v423 (S (Z)))))
+  (substitution (@v424 (Z)) (@v425 (S (Z))) (@v426 t0)))
 (let t0 (map-of (Z) (S (Z))))
 (let t1 (HasMap t0))
 (Rule
@@ -42,7 +42,7 @@ expression: proof_snapshot
     (Fiat (= (S (Z)) (S (Z))))
     (Eval)
     (Fiat (= t1 t1)))
-  (substitution (@v575 (Z)) (@v576 (S (Z))) (@v577 t0)))
+  (substitution (@v578 (S (Z))) (@v577 (Z)) (@v579 t0)))
 (let prf0 (Fiat (= (Z) (Z))))
 (let t0 (multiset-of (S (Z)) (Z) (Z)))
 (let t1 (HasMS t0))
@@ -50,7 +50,7 @@ expression: proof_snapshot
   (= (@ExistsConstructor4) (@ExistsConstructor4))
   (name "@prove_exists_rule4")
   (premises prf0 (Fiat (= (S (Z)) (S (Z)))) prf0 (Eval) (Fiat (= t1 t1)))
-  (substitution (@v722 (S (Z))) (@v721 (Z)) (@v724 t0) (@v723 (Z))))
+  (substitution (@v725 (Z)) (@v726 t0) (@v724 (S (Z))) (@v723 (Z))))
 (let t0 (vec-of (Z) (S (Z))))
 (let t1 (HasVec t0))
 (Rule
@@ -94,7 +94,7 @@ expression: proof_snapshot
       ((MapGet w))
          )")
   (premises (Fiat (= t1 t1)) (Fiat (= (Z) (Z))) (Fiat (= (S (Z)) (S (Z)))))
-  (substitution (m t0) (@v1079 (Z)) (w (S (Z)))))
+  (substitution (m t0) (@v1085 (Z)) (w (S (Z)))))
 (let t0 (multiset-of (S (Z)) (Z) (Z)))
 (let t1 (HasMS t0))
 (Rule
@@ -195,5 +195,5 @@ expression: proof_snapshot
       ((OutWrap w))
          )")
       (premises (Fiat (= (HasElem (Z)) (HasElem (Z)))) (Eval) (Fiat (= t0 t0)))
-      (substitution (a (Z)) (w t0) (@v2050 (vec-of (Z) (Z))))))
-  (substitution (@v2086 (Z)) (@v2087 (vec-of (Z) (Z))) (@v2085 (Z))))
+      (substitution (a (Z)) (@v2068 (vec-of (Z) (Z))) (w t0))))
+  (substitution (@v2104 (Z)) (@v2103 (Z)) (@v2105 (vec-of (Z) (Z)))))
diff --git a/egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap b/egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap
index 3f653318..af4759dc 100644
--- a/egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap
+++ b/egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap
@@ -100,7 +100,7 @@ expression: proof_snapshot
             (substitution (x (N 2)) (@rewrite_var__ (Id (N 2)))))
           1))
       0))
-  (substitution (@v1106 (N 2)) (@v1107 t3) (@v1105 (N 1))))
+  (substitution (@v1112 (N 2)) (@v1111 (N 1)) (@v1113 t3)))
 (let t0 (Add (Num 51) (Num 52)))
 (let t1 (Add (Num 52) (Num 51)))
 (let t2 (premises (Fiat (= (Go) (Go)))))
@@ -147,7 +147,7 @@ expression: proof_snapshot
         prf0
         0)
       0))
-  (substitution (@v1169 t1) (@v1170 t5)))
+  (substitution (@v1176 t5) (@v1175 t1)))
 (let t0 (premises (Fiat (= (Go) (Go)))))
 (let prf0
   (Rule
@@ -249,7 +249,7 @@ expression: proof_snapshot
             (substitution (x (N 12)) (@rewrite_var__ (Id (N 12)))))
           1))
       0))
-  (substitution (@v1231 (N 11)) (@v1232 (N 11)) (@v1234 t3) (@v1233 (N 12))))
+  (substitution (@v1239 (N 12)) (@v1240 t3) (@v1237 (N 11)) (@v1238 (N 11))))
 (let t0 (premises (Fiat (= (Go) (Go)))))
 (let prf0
   (Rule
@@ -344,11 +344,11 @@ expression: proof_snapshot
           0))
       0))
   (substitution
-    (@v1308 (N 23))
-    (@v1307 (N 22))
-    (@v1305 (N 21))
-    (@v1306 (N 23))
-    (@v1309 t3)))
+    (@v1312 (N 23))
+    (@v1314 (N 23))
+    (@v1311 (N 21))
+    (@v1315 t3)
+    (@v1313 (N 22))))
 (let t0 (premises (Fiat (= (Go) (Go)))))
 (let prf0
   (Rule
@@ -418,7 +418,7 @@ expression: proof_snapshot
         prf1
         1)
       0))
-  (substitution (@v1389 (N 31)) (@v1390 (N 31)) (@v1391 (N 32)) (@v1392 t3)))
+  (substitution (@v1396 (N 31)) (@v1395 (N 31)) (@v1397 (N 32)) (@v1398 t3)))
 (let t0 (premises (Fiat (= (Go) (Go)))))
 (let prf0
   (Rule
@@ -526,4 +526,4 @@ expression: proof_snapshot
           0)
         1)
       0))
-  (substitution (@v1465 (N 41)) (@v1463 (N 41)) (@v1464 (N 42)) (@v1466 t5)))
+  (substitution (@v1469 (N 41)) (@v1471 (N 41)) (@v1470 (N 42)) (@v1472 t5)))
diff --git a/egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap b/egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap
index 01496689..fe1ff58c 100644
--- a/egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap
+++ b/egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap
@@ -21,7 +21,7 @@ expression: proof_snapshot
     (Trans (= t0 t0) (Sym (= t0 t1) prf0) prf0)
     (Fiat (= (N 1) (N 1)))
     (Eval))
-  (substitution (@n (set-of (N 1))) (@v136 (N 1))))
+  (substitution (@n (set-of (N 1))) (@v138 (N 1))))
 (let t0 (set-of (N 1) (N 3)))
 (let t1 (freer (N 0) t0))
 (let t2 (freer (N 0) (set-of (N 1))))
@@ -49,4 +49,4 @@ expression: proof_snapshot
     (Fiat (= (N 1) (N 1)))
     (Fiat (= (N 3) (N 3)))
     (Eval))
-  (substitution (@v235 (N 1)) (@v236 (N 3)) (@n1 t0)))
+  (substitution (@v237 (N 1)) (@v238 (N 3)) (@n1 t0)))
diff --git a/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap b/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap
index fee6d239..7d68eaca 100644
--- a/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap
+++ b/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap
@@ -1,6 +1,5 @@
 ---
 source: egglog/tests/files.rs
-assertion_line: 279
 expression: proof_snapshot
 ---
 (let t0 (Mul (Num 2) (Add (Var "x") (Num 3))))
diff --git a/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap b/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap
index fee6d239..7d68eaca 100644
--- a/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap
+++ b/egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap
@@ -1,6 +1,5 @@
 ---
 source: egglog/tests/files.rs
-assertion_line: 279
 expression: proof_snapshot
 ---
 (let t0 (Mul (Num 2) (Add (Var "x") (Num 3))))
diff --git a/egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap b/egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap
index 2509796c..40116635 100644
--- a/egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap
+++ b/egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap
@@ -23,4 +23,8 @@ expression: proof_snapshot
   (= (@ExistsConstructor16) (@ExistsConstructor16))
   (name "@prove_exists_rule16")
   (premises prf0 (Fiat (= (Val 2) (Val 2))) prf0 prf0 (Fiat (= () ())))
-  (substitution (@v991 (Val 1)) (@v990 (Val 2)) (@v989 (Val 1)) (@v992 (Val 1))))
+  (substitution
+    (@v998 (Val 2))
+    (@v997 (Val 1))
+    (@v999 (Val 1))
+    (@v1000 (Val 1))))
diff --git a/egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap b/egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap
index 06d47a79..63b11f13 100644
--- a/egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap
+++ b/egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap
@@ -165,4 +165,4 @@ expression: proof_snapshot
           (x3 (Var "b3"))
           t2)))
     (Fiat (= () ())))
-  (substitution (@v834 t3) (@v833 t0)))
+  (substitution (@v840 t3) (@v839 t0)))
diff --git a/egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap b/egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap
index c9786285..3da9a16b 100644
--- a/egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap
+++ b/egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap
@@ -27,4 +27,4 @@ expression: proof_snapshot
           0)
         0)
       0))
-  (substitution (@rewrite_var__1 t1) (@v80 (vec-of (vec-of (b)))) (@v79 (b))))
+  (substitution (@v81 (b)) (@rewrite_var__1 t1) (@v82 (vec-of (vec-of (b))))))
diff --git a/egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap b/egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap
index b12cb48a..10986590 100644
--- a/egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap
+++ b/egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap
@@ -257,5 +257,5 @@ expression: proof_snapshot
           (t1 (Type "struct s*")))))
     (Fiat (= () ())))
   (substitution
-    (@v3842 (expr-points-to (Expr "u")))
-    (@v3843 (expr-points-to (Expr "sp")))))
+    (@v3936 (expr-points-to (Expr "u")))
+    (@v3937 (expr-points-to (Expr "sp")))))