diff --git a/egglog-bridge/examples/ac.rs b/egglog-bridge/examples/ac.rs
index e6a83b16e..f05b792cb 100644
--- a/egglog-bridge/examples/ac.rs
+++ b/egglog-bridge/examples/ac.rs
@@ -16,6 +16,8 @@ fn main() {
         let int_base = egraph.base_values_mut().register_type::<i64>();
         let num_table = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "num".into(),
@@ -23,6 +25,8 @@ fn main() {
         });
         let add_table = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Id; 3],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "add".into(),
diff --git a/egglog-bridge/examples/math.rs b/egglog-bridge/examples/math.rs
index 8c0eaa13b..12779a246 100644
--- a/egglog-bridge/examples/math.rs
+++ b/egglog-bridge/examples/math.rs
@@ -21,6 +21,8 @@ fn main() {
         // tables
         let diff = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "diff".into(),
@@ -28,6 +30,8 @@ fn main() {
         });
         let integral = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "integral".into(),
@@ -36,6 +40,8 @@ fn main() {
 
         let add = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "add".into(),
@@ -43,6 +49,8 @@ fn main() {
         });
         let sub = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "sub".into(),
@@ -51,6 +59,8 @@ fn main() {
 
         let mul = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "mul".into(),
@@ -59,6 +69,8 @@ fn main() {
 
         let div = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "div".into(),
@@ -67,6 +79,8 @@ fn main() {
 
         let pow = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "pow".into(),
@@ -75,6 +89,8 @@ fn main() {
 
         let ln = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Id, ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "ln".into(),
@@ -83,6 +99,8 @@ fn main() {
 
         let sqrt = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Id, ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "sqrt".into(),
@@ -91,6 +109,8 @@ fn main() {
 
         let sin = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Id, ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "sin".into(),
@@ -99,6 +119,8 @@ fn main() {
 
         let cos = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Id, ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "cos".into(),
@@ -107,6 +129,8 @@ fn main() {
 
         let rat = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Base(rational_ty), ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "rat".into(),
@@ -115,6 +139,8 @@ fn main() {
 
         let var = egraph.add_table(FunctionConfig {
             schema: vec![ColumnTy::Base(string_ty), ColumnTy::Id],
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "var".into(),
diff --git a/egglog-bridge/src/lib.rs b/egglog-bridge/src/lib.rs
index 0997a3cf8..52f9e5107 100644
--- a/egglog-bridge/src/lib.rs
+++ b/egglog-bridge/src/lib.rs
@@ -190,8 +190,25 @@ impl Default for EGraph {
 
 /// Properties of a function added to an [`EGraph`].
 pub struct FunctionConfig {
-    /// The function's schema. The last column in the schema is the return type.
+    /// The function's schema. The last `num_values` columns are the value
+    /// (return) columns; the rest are keys.
     pub schema: Vec<ColumnTy>,
+    /// Number of value (non-key) columns. Defaults conceptually to 1; set
+    /// higher for functions whose value compiles to multiple columns.
+    pub num_values: usize,
+    /// Optional merge short-circuit on row identity. When `Some(k)`, a key collision
+    /// whose leading `k` value columns are unchanged is a no-op: the existing row is
+    /// kept verbatim and the merge body (and its side effects) does not run. Trailing
+    /// value columns beyond the first `k` ride along from the surviving row.
+    ///
+    /// `None` (the default) keeps the classic behavior: the merge body always runs and
+    /// `changed` is computed from the result (preserved exactly for ordinary functions,
+    /// including `Const` merges that can change the row even when `cur == new`).
+    ///
+    /// The motivating case is the proof-encoding FD view, whose merge body mints
+    /// proof/term nodes as a side effect; `Some(1)` lets it match normal egglog's
+    /// `cur == new` short-circuit despite carrying an extra proof column or minting body.
+    pub identity_values: Option<usize>,
     /// The behavior of the function when lookups are made on keys not currently present.
     pub default: DefaultVal,
     /// How to resolve FD conflicts for the function.
@@ -335,6 +352,8 @@ impl EGraph {
             let schema_math = SchemaMath {
                 subsume: table_info.can_subsume,
                 func_cols: table_info.schema.len(),
+                num_values: table_info.num_values,
+                identity_values: table_info.identity_values,
             };
             let table_id = table_info.table;
             extended_row.extend_from_slice(&row);
@@ -365,6 +384,8 @@ impl EGraph {
         let schema_math = SchemaMath {
             subsume: info.can_subsume,
             func_cols: info.schema.len(),
+            num_values: info.num_values,
+            identity_values: info.identity_values,
         };
         let mut extended_row = Vec::new();
         extended_row.extend_from_slice(inputs);
@@ -391,6 +412,8 @@ impl EGraph {
         let schema_math = SchemaMath {
             subsume: info.can_subsume,
             func_cols: info.schema.len(),
+            num_values: info.num_values,
+            identity_values: info.identity_values,
         };
         let table_id = info.table;
         let table = self.db.get_table(table_id);
@@ -441,6 +464,8 @@ impl EGraph {
         let schema_math = SchemaMath {
             subsume: info.can_subsume,
             func_cols: info.schema.len(),
+            num_values: info.num_values,
+            identity_values: info.identity_values,
         };
         let imp = self.db.get_table(table);
         let all = imp.all();
@@ -507,11 +532,23 @@ impl EGraph {
     pub fn add_table(&mut self, config: FunctionConfig) -> FunctionId {
         let FunctionConfig {
             schema,
+            num_values,
+            identity_values,
             default,
             merge,
             name,
             can_subsume,
         } = config;
+        assert!(
+            num_values >= 1 && num_values <= schema.len(),
+            "num_values must be >=1 and not exceed the column count"
+        );
+        if let Some(k) = identity_values {
+            assert!(
+                k >= 1 && k <= num_values,
+                "identity_values must be >=1 and not exceed num_values"
+            );
+        }
         assert!(
             !schema.is_empty(),
             "must have at least one column in schema"
@@ -525,6 +562,8 @@ impl EGraph {
         let schema_math = SchemaMath {
             subsume: can_subsume,
             func_cols: schema.len(),
+            num_values,
+            identity_values,
         };
         let n_args = schema_math.num_keys();
         let n_cols = schema_math.table_columns();
@@ -551,6 +590,8 @@ impl EGraph {
         let res = self.funcs.push(FunctionInfo {
             table: table_id,
             schema: schema.clone(),
+            num_values,
+            identity_values,
             incremental_rebuild_rules: Default::default(),
             nonincremental_rebuild_rule: RuleId::new(!0),
             default_val: default,
@@ -983,6 +1024,12 @@ struct CachedPlanInfo {
 struct FunctionInfo {
     table: TableId,
     schema: Vec<ColumnTy>,
+    /// Number of value (non-key) columns; the last `num_values` columns of
+    /// `schema` are the function's value. Usually 1.
+    num_values: usize,
+    /// Optional merge short-circuit on row identity (see
+    /// [`FunctionConfig::identity_values`]).
+    identity_values: Option<usize>,
     incremental_rebuild_rules: Vec<RuleId>,
     nonincremental_rebuild_rule: RuleId,
     default_val: DefaultVal,
@@ -1008,6 +1055,7 @@ pub enum DefaultVal {
 }
 
 /// How to resolve FD conflicts for a table.
+#[derive(Clone)]
 pub enum MergeFn {
     /// Panic if the old and new values don't match.
     AssertEq,
@@ -1019,14 +1067,39 @@ pub enum MergeFn {
     /// The output of a merge is determined by looking up the value for the given function and the
     /// given arguments in the egraph.
     Function(FunctionId, Vec<MergeFn>),
-    /// Always return the old value for the given function.
+    /// Always return the old value for the given function (value column 0).
     Old,
-    /// Always return the new value for the given function.
+    /// Always return the new value for the given function (value column 0).
     New,
+    /// The old value of value column `i` (for multi-value functions). `Old` is
+    /// `OldCol(0)`.
+    OldCol(usize),
+    /// The new value of value column `i` (for multi-value functions). `New` is
+    /// `NewCol(0)`.
+    NewCol(usize),
+    /// A multi-value result: one merge function per value column. Used as the
+    /// top-level merge of a function with more than one value column; each
+    /// element may read any column via `OldCol`/`NewCol`. Not nested.
+    Tuple(Vec<MergeFn>),
     /// Always overwrite the new value for the given function with a constant. This is more useful
     /// as a "base case" in a more complicated merge function (e.g. one that clamps a value between
     /// 1 and 100) than it is as a standalone merge function.
     Const(Value),
+    /// Insert a row into the given function's table (the args evaluate to the
+    /// full row), respecting that table's own merge. Returns the old value
+    /// (its return is meant to be discarded inside a [`MergeFn::Seq`]). Used to
+    /// model a `(set (f ...) v)` action inside a merge; declares `f`'s table as
+    /// a write-dependency so the side write is safe during batched merges.
+    TableInsert(FunctionId, Vec<MergeFn>),
+    /// Evaluate each merge function in order (for their effects) and return the
+    /// value of the last one. Models an action-block merge: the leading entries
+    /// are effects (e.g. [`MergeFn::TableInsert`]) and the last is the value.
+    Seq(Vec<MergeFn>),
+    /// Mint a pair-valued constructor inside a merge and return its output e-class.
+    /// `args` evaluate to the key (children); the first value column (the output) is
+    /// minted (`FreshId`) and the rest are written from `value_args` (e.g. the proof).
+    /// Used by the FD proof encoding. See [`TableAction::lookup_or_insert_multi`].
+    Construct(FunctionId, Vec<MergeFn>, Vec<MergeFn>),
 }
 
 impl MergeFn {
@@ -1052,7 +1125,32 @@ impl MergeFn {
             UnionId => {
                 write_deps.insert(egraph.uf_table);
             }
-            AssertEq | Old | New | Const(..) => {}
+            TableInsert(func, args) => {
+                // The side write makes the target table a write-dependency, so
+                // its buffer is pre-allocated during batched merges (the whole
+                // reason this exists rather than a by-name primitive insert).
+                write_deps.insert(egraph.funcs[*func].table);
+                args.iter()
+                    .for_each(|arg| arg.fill_deps(egraph, read_deps, write_deps));
+            }
+            Seq(items) => {
+                items
+                    .iter()
+                    .for_each(|item| item.fill_deps(egraph, read_deps, write_deps));
+            }
+            Tuple(items) => {
+                items
+                    .iter()
+                    .for_each(|item| item.fill_deps(egraph, read_deps, write_deps));
+            }
+            Construct(func, args, value_args) => {
+                read_deps.insert(egraph.funcs[*func].table);
+                write_deps.insert(egraph.funcs[*func].table);
+                args.iter()
+                    .chain(value_args.iter())
+                    .for_each(|arg| arg.fill_deps(egraph, read_deps, write_deps));
+            }
+            AssertEq | Old | New | OldCol(_) | NewCol(_) | Const(..) => {}
         }
     }
 
@@ -1066,34 +1164,71 @@ impl MergeFn {
 
         Box::new(move |state, cur, new, out| {
             let timestamp = new[schema_math.ts_col()];
+            let vcols = schema_math.value_cols();
+            let cur_vals = &cur[vcols.clone()];
+            let new_vals = &new[vcols.clone()];
 
             let mut changed = false;
 
-            let ret_val = {
-                let cur = cur[schema_math.ret_val_col()];
-                let new = new[schema_math.ret_val_col()];
-                let out = resolved.run(state, cur, new, timestamp);
-                changed |= cur != out;
-                out
+            // Identity-column short-circuit (`identity_values == Some(k)`): a collision
+            // leaving the leading `k` value columns unchanged keeps the existing row
+            // verbatim and skips the merge body, mirroring normal egglog's `cur == new`
+            // short-circuit on the identity columns alone. Ordinary functions use `None`
+            // and run the body unconditionally.
+            //
+            // Subsumption is still combined here, since it is independent of the value
+            // columns.
+            let identity_unchanged = schema_math
+                .identity_values
+                .is_some_and(|k| cur_vals[..k] == new_vals[..k]);
+            if identity_unchanged {
+                let subsume = schema_math.subsume.then(|| {
+                    let cur_s = cur[schema_math.subsume_col()];
+                    let new_s = new[schema_math.subsume_col()];
+                    let out_s = combine_subsumed(cur_s, new_s);
+                    changed |= cur_s != out_s;
+                    out_s
+                });
+                if changed {
+                    out.extend_from_slice(cur);
+                    out[schema_math.ts_col()] = timestamp;
+                    if let Some(subsume) = subsume {
+                        out[schema_math.subsume_col()] = subsume;
+                    }
+                }
+                return changed;
+            }
+
+            // Compute the merged value column(s). A `Tuple` merge produces one
+            // value per column (each may read any old/new column); any other
+            // merge is single-valued.
+            let merged: SmallVec<[Value; 2]> = match &resolved {
+                ResolvedMergeFn::Tuple(items) => items
+                    .iter()
+                    .map(|m| m.run(state, cur_vals, new_vals, timestamp))
+                    .collect(),
+                single => SmallVec::from_elem(single.run(state, cur_vals, new_vals, timestamp), 1),
             };
+            for (k, v) in merged.iter().enumerate() {
+                changed |= cur_vals[k] != *v;
+            }
 
             let subsume = schema_math.subsume.then(|| {
                 let cur = cur[schema_math.subsume_col()];
                 let new = new[schema_math.subsume_col()];
-                let out = combine_subsumed(cur, new);
-                changed |= cur != out;
-                out
+                let out_s = combine_subsumed(cur, new);
+                changed |= cur != out_s;
+                out_s
             });
             if changed {
                 out.extend_from_slice(new);
-                schema_math.write_table_row(
-                    out,
-                    RowVals {
-                        timestamp,
-                        subsume,
-                        ret_val: Some(ret_val),
-                    },
-                );
+                for (k, col) in vcols.enumerate() {
+                    out[col] = merged[k];
+                }
+                out[schema_math.ts_col()] = timestamp;
+                if let Some(subsume) = subsume {
+                    out[schema_math.subsume_col()] = subsume;
+                }
             }
 
             changed
@@ -1103,8 +1238,16 @@ impl MergeFn {
     fn resolve(&self, function_name: &str, egraph: &mut EGraph) -> ResolvedMergeFn {
         match self {
             MergeFn::Const(v) => ResolvedMergeFn::Const(*v),
-            MergeFn::Old => ResolvedMergeFn::Old,
-            MergeFn::New => ResolvedMergeFn::New,
+            MergeFn::Old => ResolvedMergeFn::OldCol(0),
+            MergeFn::New => ResolvedMergeFn::NewCol(0),
+            MergeFn::OldCol(i) => ResolvedMergeFn::OldCol(*i),
+            MergeFn::NewCol(i) => ResolvedMergeFn::NewCol(*i),
+            MergeFn::Tuple(items) => ResolvedMergeFn::Tuple(
+                items
+                    .iter()
+                    .map(|item| item.resolve(function_name, egraph))
+                    .collect(),
+            ),
             MergeFn::AssertEq => ResolvedMergeFn::AssertEq {
                 panic: egraph.new_panic(format!(
                     "Illegal merge attempted for function {function_name}"
@@ -1147,6 +1290,46 @@ impl MergeFn {
                         .collect::<Vec<_>>(),
                 }
             }
+            MergeFn::TableInsert(func, args) => ResolvedMergeFn::TableInsert {
+                table: TableAction::new(egraph, *func),
+                args: args
+                    .iter()
+                    .map(|arg| arg.resolve(function_name, egraph))
+                    .collect::<Vec<_>>(),
+            },
+            MergeFn::Seq(items) => ResolvedMergeFn::Seq(
+                items
+                    .iter()
+                    .map(|item| item.resolve(function_name, egraph))
+                    .collect::<Vec<_>>(),
+            ),
+            MergeFn::Construct(func, args, value_args) => {
+                let func_info = &egraph.funcs[*func];
+                debug_assert_eq!(
+                    func_info.schema.len(),
+                    args.len() + func_info.num_values,
+                    "Construct for {function_name}: key arity must be schema minus value columns for {}",
+                    func_info.name
+                );
+                debug_assert_eq!(
+                    value_args.len() + 1,
+                    func_info.num_values,
+                    "Construct for {function_name}: value_args must fill every value column \
+                     except the minted output for {}",
+                    func_info.name
+                );
+                ResolvedMergeFn::Construct {
+                    table: TableAction::new(egraph, *func),
+                    args: args
+                        .iter()
+                        .map(|arg| arg.resolve(function_name, egraph))
+                        .collect::<Vec<_>>(),
+                    value_args: value_args
+                        .iter()
+                        .map(|arg| arg.resolve(function_name, egraph))
+                        .collect::<Vec<_>>(),
+                }
+            }
         }
     }
 }
@@ -1157,8 +1340,12 @@ impl MergeFn {
 /// holding onto any references, so it can be `move`d inside the `core_relations::MergeFn`.
 enum ResolvedMergeFn {
     Const(Value),
-    Old,
-    New,
+    /// Old value of value column `i`.
+    OldCol(usize),
+    /// New value of value column `i`.
+    NewCol(usize),
+    /// Per-value-column merges (top-level for multi-value functions).
+    Tuple(Vec<ResolvedMergeFn>),
     AssertEq {
         panic: ExternalFunctionId,
     },
@@ -1175,29 +1362,46 @@ enum ResolvedMergeFn {
         args: Vec<ResolvedMergeFn>,
         panic: ExternalFunctionId,
     },
+    TableInsert {
+        table: TableAction,
+        args: Vec<ResolvedMergeFn>,
+    },
+    Seq(Vec<ResolvedMergeFn>),
+    Construct {
+        table: TableAction,
+        args: Vec<ResolvedMergeFn>,
+        value_args: Vec<ResolvedMergeFn>,
+    },
 }
 
 impl ResolvedMergeFn {
-    fn run(&self, state: &mut ExecutionState, cur: Value, new: Value, ts: Value) -> Value {
+    /// Evaluate one value column's merge. `cur`/`new` are the old/new *value
+    /// tuples* (the value columns of the conflicting rows); single-value
+    /// functions pass a one-element slice, so `OldCol(0)`/`NewCol(0)` recover
+    /// the classic `old`/`new`.
+    fn run(&self, state: &mut ExecutionState, cur: &[Value], new: &[Value], ts: Value) -> Value {
         match self {
             ResolvedMergeFn::Const(v) => *v,
-            ResolvedMergeFn::Old => cur,
-            ResolvedMergeFn::New => new,
+            ResolvedMergeFn::OldCol(i) => cur[*i],
+            ResolvedMergeFn::NewCol(i) => new[*i],
+            ResolvedMergeFn::Tuple(_) => {
+                unreachable!("a Tuple merge is handled by to_callback, never nested/run directly")
+            }
             ResolvedMergeFn::AssertEq { panic } => {
                 if cur != new {
                     let res = state.call_external_func(*panic, &[]);
                     assert_eq!(res, None);
                 }
-                cur
+                cur[0]
             }
             ResolvedMergeFn::UnionId { uf_table } => {
-                if cur != new {
-                    state.stage_insert(*uf_table, &[cur, new, ts]);
-                    // We pick the minimum when unioning. This matches the original egglog
-                    // behavior. THIS MUST MATCH THE UNION-FIND IMPLEMENTATION!
-                    std::cmp::min(cur, new)
+                if cur[0] != new[0] {
+                    state.stage_insert(*uf_table, &[cur[0], new[0], ts]);
+                    // Pick the minimum when unioning; this must match the original
+                    // egglog behavior and the union-find implementation.
+                    std::cmp::min(cur[0], new[0])
                 } else {
-                    cur
+                    cur[0]
                 }
             }
             // NB: The primitive and function-based merge functions heap allocate a single callback
@@ -1215,14 +1419,14 @@ impl ResolvedMergeFn {
                     None => {
                         let res = state.call_external_func(*panic, &[]);
                         assert_eq!(res, None);
-                        cur
+                        cur[0]
                     }
                 }
             }
             ResolvedMergeFn::Function { func, args, panic } => {
                 // see github.com/egraphs-good/egglog/pull/287
                 if cur == new {
-                    return cur;
+                    return cur[0];
                 }
 
                 let args = args
@@ -1238,9 +1442,45 @@ impl ResolvedMergeFn {
                 func.lookup_or_insert(state, &args).unwrap_or_else(|| {
                     let res = state.call_external_func(*panic, &[]);
                     assert_eq!(res, None);
-                    cur
+                    cur[0]
                 })
             }
+            ResolvedMergeFn::TableInsert { table, args } => {
+                let row = args
+                    .iter()
+                    .map(|arg| arg.run(state, cur, new, ts))
+                    .collect::<Vec<_>>();
+                // Insert respects the target table's own merge; the timestamp
+                // column is appended by `TableAction::insert`.
+                table.insert(state, row.into_iter());
+                // Return value is discarded by the enclosing `Seq`.
+                cur[0]
+            }
+            ResolvedMergeFn::Seq(items) => {
+                let mut result = cur[0];
+                for item in items {
+                    result = item.run(state, cur, new, ts);
+                }
+                result
+            }
+            ResolvedMergeFn::Construct {
+                table,
+                args,
+                value_args,
+            } => {
+                let key = args
+                    .iter()
+                    .map(|arg| arg.run(state, cur, new, ts))
+                    .collect::<SmallVec<[Value; 4]>>();
+                let vals = value_args
+                    .iter()
+                    .map(|arg| arg.run(state, cur, new, ts))
+                    .collect::<SmallVec<[Value; 4]>>();
+                // Constructor: always mints on miss, so this is `Some`.
+                table
+                    .lookup_or_insert_multi(state, &key, &vals)
+                    .unwrap_or(cur[0])
+            }
         }
     }
 }
@@ -1266,6 +1506,8 @@ impl TableAction {
             table_math: SchemaMath {
                 func_cols: func_info.schema.len(),
                 subsume: func_info.can_subsume,
+                num_values: func_info.num_values,
+                identity_values: func_info.identity_values,
             },
             default: match &func_info.default_val {
                 DefaultVal::FreshId => Some(MergeVal::Counter(egraph.id_counter)),
@@ -1331,6 +1573,48 @@ impl TableAction {
         }
     }
 
+    /// Multi-value variant of [`TableAction::lookup_or_insert`] for a pair-valued
+    /// constructor `(children) -> (output, extra...)`: the first value column
+    /// (`output`) is minted (the configured `FreshId` default) and the rest are written
+    /// from `provided_vals` (e.g. the proof). Returns the minted `output`.
+    ///
+    /// Idempotent: an already-present key returns its existing `output` and writes
+    /// nothing, so it can be evaluated more than once and yield the same id. This is a
+    /// write operation, only safe in action/merge contexts.
+    pub fn lookup_or_insert_multi(
+        &self,
+        state: &mut ExecutionState,
+        key: &[Value],
+        provided_vals: &[Value],
+    ) -> Option<Value> {
+        match self.default {
+            Some(default) => {
+                debug_assert_eq!(
+                    self.table_math.num_values,
+                    1 + provided_vals.len(),
+                    "lookup_or_insert_multi: provided_vals must fill every value \
+                     column except the minted first one"
+                );
+                let timestamp =
+                    MergeVal::Constant(Value::from_usize(state.read_counter(self.timestamp)));
+                // Non-key columns, in order: [output (minted), provided.., ts, subsume?].
+                let mut merge_vals = SmallVec::<[MergeVal; 4]>::new();
+                merge_vals.push(default);
+                merge_vals.extend(provided_vals.iter().map(|v| MergeVal::Constant(*v)));
+                merge_vals.push(timestamp);
+                if self.table_math.subsume {
+                    merge_vals.push(MergeVal::Constant(NOT_SUBSUMED));
+                }
+                // The first value column is at `num_keys()`.
+                Some(
+                    state.predict_val(self.table, key, merge_vals.iter().copied())
+                        [self.table_math.num_keys()],
+                )
+            }
+            None => self.lookup(state, key),
+        }
+    }
+
     /// Insert a row into this table.
     pub fn insert(&self, state: &mut ExecutionState, row: impl Iterator<Item = Value>) {
         let ts = Value::from_usize(state.read_counter(self.timestamp));
@@ -1544,8 +1828,14 @@ fn combine_subsumed(v1: Value, v2: Value) -> Value {
 struct SchemaMath {
     /// Whether or not the table is enabled for subsumption.
     subsume: bool,
-    /// The number of columns in the function (including the return value).
+    /// The number of columns in the function (keys + all value columns).
     func_cols: usize,
+    /// The number of value (non-key) columns. Almost always 1; functions whose
+    /// value is compiled to multiple columns (e.g. an unboxed pair) have more.
+    num_values: usize,
+    /// Optional merge short-circuit on row identity (see
+    /// [`FunctionConfig::identity_values`]). `None` for ordinary functions.
+    identity_values: Option<usize>,
 }
 
 /// A struct containing possible non-key portions of a table row. To be used with
@@ -1595,14 +1885,25 @@ impl SchemaMath {
     }
 
     fn num_keys(&self) -> usize {
-        self.func_cols - 1
+        self.func_cols - self.num_values
     }
 
     fn table_columns(&self) -> usize {
         self.func_cols + 1 /* timestamp */ + if self.subsume { 1 } else { 0 }
     }
 
+    /// The column indices of the value (non-key) columns: `num_keys..func_cols`.
+    #[allow(dead_code)]
+    fn value_cols(&self) -> std::ops::Range<usize> {
+        self.num_keys()..self.func_cols
+    }
+
+    /// The single value column. Only valid when `num_values == 1`.
     fn ret_val_col(&self) -> usize {
+        debug_assert_eq!(
+            self.num_values, 1,
+            "ret_val_col requires a single value column"
+        );
         self.func_cols - 1
     }
 
diff --git a/egglog-bridge/src/rule.rs b/egglog-bridge/src/rule.rs
index 8a4a7da12..f676eb32e 100644
--- a/egglog-bridge/src/rule.rs
+++ b/egglog-bridge/src/rule.rs
@@ -171,6 +171,16 @@ impl RuleBuilder<'_> {
         self.egraph
     }
 
+    /// Constrain two query entries to be equal.
+    pub fn assert_eq_entries(&mut self, l: QueryEntry, r: QueryEntry) {
+        self.add_callback(move |inner, rb| {
+            let l = inner.convert(&l);
+            let r = inner.convert(&r);
+            rb.assert_eq(l, r);
+            Ok(())
+        });
+    }
+
     /// Register a runtime panic with a custom message and return its
     /// id. When called via [`call_external_func`], the panic writes
     /// the message to the egraph's panic side channel and triggers
@@ -360,11 +370,15 @@ impl RuleBuilder<'_> {
             SchemaMath {
                 subsume: info.can_subsume,
                 func_cols: info.schema.len(),
+                num_values: info.num_values,
+                identity_values: info.identity_values,
             }
         } else {
             SchemaMath {
                 subsume: subsume_entry.is_some(),
                 func_cols: entries.len(),
+                num_values: 1,
+                identity_values: None,
             }
         };
         schema_math.write_table_row(
@@ -473,6 +487,18 @@ impl RuleBuilder<'_> {
     ///
     /// `entries` should match the number of keys to the function.
     pub fn subsume(&mut self, func: FunctionId, entries: &[QueryEntry]) {
+        let info = &self.egraph.funcs[func];
+        assert!(info.can_subsume);
+        if info.num_values == 1 {
+            self.subsume_single_value(func, entries);
+        } else {
+            self.subsume_multi_value(func, entries);
+        }
+    }
+
+    /// Single-value subsume: insert a subsumed row if the tuple is new (via
+    /// `lookup_with_subsumed` with `SUBSUMED`), then re-insert it subsumed.
+    fn subsume_single_value(&mut self, func: FunctionId, entries: &[QueryEntry]) {
         // First, insert a subsumed value if the tuple is new.
         let ret = self.lookup_with_subsumed(
             func,
@@ -487,13 +513,73 @@ impl RuleBuilder<'_> {
         let schema_math = SchemaMath {
             subsume: info.can_subsume,
             func_cols: info.schema.len(),
+            num_values: info.num_values,
+            identity_values: info.identity_values,
         };
-        assert!(info.can_subsume);
         assert_eq!(entries.len() + 1, info.schema.len());
         let entries = entries.to_vec();
         let table = info.table;
-
         let ret: QueryEntry = ret.into();
+        self.add_callback(move |inner, rb| {
+            let mut dst_entries = inner.convert_all(&entries);
+            let cur_subsume_val = rb.lookup(
+                table,
+                &dst_entries,
+                ColumnId::from_usize(schema_math.subsume_col()),
+            )?;
+            schema_math.write_table_row(
+                &mut dst_entries,
+                RowVals {
+                    timestamp: inner.next_ts(),
+                    subsume: Some(SUBSUMED.into()),
+                    ret_val: Some(inner.convert(&ret)),
+                },
+            );
+            rb.insert_if_eq(
+                table,
+                cur_subsume_val.into(),
+                NOT_SUBSUMED.into(),
+                &dst_entries,
+            )?;
+            Ok(())
+        });
+    }
+
+    /// Multi-value subsume: read each value column (inserting a subsumed
+    /// default row if the tuple is new), then re-insert the row subsumed.
+    fn subsume_multi_value(&mut self, func: FunctionId, entries: &[QueryEntry]) {
+        let info = &self.egraph.funcs[func];
+        let schema_math = SchemaMath {
+            subsume: info.can_subsume,
+            func_cols: info.schema.len(),
+            num_values: info.num_values,
+            identity_values: info.identity_values,
+        };
+        assert_eq!(
+            entries.len(),
+            schema_math.num_keys(),
+            "subsume expects the key columns of {func:?}"
+        );
+        // Read back each value column, inserting a SUBSUMED default row if the
+        // tuple is new so that a fresh subsume is honored.
+        let value_vals: Vec<QueryEntry> = (0..info.num_values)
+            .map(|i| {
+                self.lookup_value_col_with_subsumed(
+                    func,
+                    entries,
+                    i,
+                    QueryEntry::Const {
+                        val: SUBSUMED,
+                        ty: ColumnTy::Id,
+                    },
+                    || "subsumed a nonexistent row!".to_string(),
+                )
+                .into()
+            })
+            .collect();
+        let table = self.egraph.funcs[func].table;
+        let entries = entries.to_vec();
+
         self.add_callback(move |inner, rb| {
             // Then, add a tuple subsuming the entry, but only if the entry isn't already subsumed.
             // Look up the current subsume value.
@@ -503,12 +589,16 @@ impl RuleBuilder<'_> {
                 &dst_entries,
                 ColumnId::from_usize(schema_math.subsume_col()),
             )?;
+            // Append the value columns, then timestamp + subsume flag.
+            for v in &value_vals {
+                dst_entries.push(inner.convert(v));
+            }
             schema_math.write_table_row(
                 &mut dst_entries,
                 RowVals {
                     timestamp: inner.next_ts(),
                     subsume: Some(SUBSUMED.into()),
-                    ret_val: Some(inner.convert(&ret)),
+                    ret_val: None,
                 },
             );
             rb.insert_if_eq(
@@ -543,6 +633,8 @@ impl RuleBuilder<'_> {
         let schema_math = SchemaMath {
             subsume: info.can_subsume,
             func_cols: info.schema.len(),
+            num_values: info.num_values,
+            identity_values: info.identity_values,
         };
         let cb: BuildRuleCallback = match info.default_val {
             DefaultVal::Const(_) | DefaultVal::FreshId => {
@@ -622,6 +714,113 @@ impl RuleBuilder<'_> {
         )
     }
 
+    /// Look up a single value column (`value_col`, 0-based among the value
+    /// columns) of a multi-value function. Like [`Self::lookup`] but selects an
+    /// arbitrary value column rather than asserting a single value column.
+    pub fn lookup_value_col(
+        &mut self,
+        func: FunctionId,
+        entries: &[QueryEntry],
+        value_col: usize,
+        panic_msg: impl FnOnce() -> String + Send + 'static,
+    ) -> Variable {
+        self.lookup_value_col_with_subsumed(
+            func,
+            entries,
+            value_col,
+            QueryEntry::Const {
+                val: NOT_SUBSUMED,
+                ty: ColumnTy::Id,
+            },
+            panic_msg,
+        )
+    }
+
+    /// Like [`Self::lookup_value_col`] but uses `subsumed` for the subsume
+    /// column when inserting a default row for a missing tuple.
+    pub(crate) fn lookup_value_col_with_subsumed(
+        &mut self,
+        func: FunctionId,
+        entries: &[QueryEntry],
+        value_col: usize,
+        subsumed: QueryEntry,
+        panic_msg: impl FnOnce() -> String + Send + 'static,
+    ) -> Variable {
+        let entries = entries.to_vec();
+        let info = &self.egraph.funcs[func];
+        let schema_math = SchemaMath {
+            subsume: info.can_subsume,
+            func_cols: info.schema.len(),
+            num_values: info.num_values,
+            identity_values: info.identity_values,
+        };
+        let dst_col = schema_math.num_keys() + value_col;
+        let ret_ty = info.schema[dst_col];
+        let res = self
+            .query
+            .vars
+            .push(VarInfo {
+                ty: ret_ty,
+                name: None,
+            })
+            .to_var();
+        let table = info.table;
+        let id_counter = self.query.id_counter;
+        let cb: BuildRuleCallback = match info.default_val {
+            DefaultVal::Const(_) | DefaultVal::FreshId => {
+                let wv: WriteVal = match &info.default_val {
+                    DefaultVal::Const(c) => (*c).into(),
+                    DefaultVal::FreshId => WriteVal::IncCounter(id_counter),
+                    _ => unreachable!(),
+                };
+                let get_write_vals = move |inner: &mut Bindings| {
+                    let mut write_vals = SmallVec::<[WriteVal; 4]>::new();
+                    for i in schema_math.num_keys()..schema_math.table_columns() {
+                        if i == schema_math.ts_col() {
+                            write_vals.push(inner.next_ts().into());
+                        } else if schema_math.subsume && i == schema_math.subsume_col() {
+                            write_vals.push(inner.convert(&subsumed).into());
+                        } else if schema_math.value_cols().contains(&i) {
+                            write_vals.push(wv);
+                        } else {
+                            unreachable!()
+                        }
+                    }
+                    write_vals
+                };
+                Box::new(move |inner, rb| {
+                    let write_vals = get_write_vals(inner);
+                    let dst_vars = inner.convert_all(&entries);
+                    let var = rb.lookup_or_insert(
+                        table,
+                        &dst_vars,
+                        &write_vals,
+                        ColumnId::from_usize(dst_col),
+                    )?;
+                    inner.mapping.insert(res.id, var.into());
+                    Ok(())
+                })
+            }
+            DefaultVal::Fail => {
+                let panic_func = self.egraph.new_panic_lazy(panic_msg);
+                Box::new(move |inner, rb| {
+                    let dst_vars = inner.convert_all(&entries);
+                    let var = rb.lookup_with_fallback(
+                        table,
+                        &dst_vars,
+                        ColumnId::from_usize(dst_col),
+                        panic_func,
+                        &[],
+                    )?;
+                    inner.mapping.insert(res.id, var.into());
+                    Ok(())
+                })
+            }
+        };
+        self.query.add_rule.push(cb);
+        res
+    }
+
     /// Merge the two values in the union-find.
     pub fn union(&mut self, l: QueryEntry, r: QueryEntry) {
         self.query.add_rule.push(Box::new(move |inner, rb| {
@@ -676,6 +875,8 @@ impl RuleBuilder<'_> {
         let schema_math = SchemaMath {
             subsume: info.can_subsume,
             func_cols: info.schema.len(),
+            num_values: info.num_values,
+            identity_values: info.identity_values,
         };
         self.query.add_rule.push(Box::new(move |inner, rb| {
             let mut dst_vars = inner.convert_all(&entries);
diff --git a/egglog-bridge/src/tests.rs b/egglog-bridge/src/tests.rs
index cbee0e87d..53c02e005 100644
--- a/egglog-bridge/src/tests.rs
+++ b/egglog-bridge/src/tests.rs
@@ -34,6 +34,8 @@ fn ac_test(can_subsume: bool) {
     let int_base = egraph.base_values_mut().register_type::<i64>();
     let num_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "num".into(),
@@ -41,6 +43,8 @@ fn ac_test(can_subsume: bool) {
     });
     let add_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id; 3],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "add".into(),
@@ -112,6 +116,8 @@ fn ac_fail() {
     let one = egraph.base_value_constant(1i64);
     let num_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "num".into(),
@@ -119,6 +125,8 @@ fn ac_fail() {
     });
     let add_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id; 3],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "add".into(),
@@ -180,6 +188,181 @@ fn ac_fail() {
     assert_ne!(canon_left, canon_right);
 }
 
+/// Minting a 2-value (output + extra) constructor view inside a custom
+/// function's `:merge` via [`MergeFn::Construct`] must write the view row (so it
+/// is queryable) and return the minted output e-class. Mirrors the Phase B FD
+/// proof encoding's `fd-mint`.
+#[test]
+fn construct_in_merge_writes_view() {
+    let mut egraph = EGraph::default();
+    let int_base = egraph.base_values_mut().register_type::<i64>();
+    // The constructor view: (child_a child_b) -> (output, extra). Two value
+    // columns; the output is the minted (FreshId) first value column.
+    let view_table = egraph.add_table(FunctionConfig {
+        schema: vec![
+            ColumnTy::Id,
+            ColumnTy::Id,
+            ColumnTy::Id,
+            ColumnTy::Base(int_base),
+        ],
+        num_values: 2,
+        identity_values: None,
+        default: DefaultVal::FreshId,
+        merge: MergeFn::Tuple(vec![MergeFn::Old, MergeFn::OldCol(1)]),
+        name: "view".into(),
+        can_subsume: false,
+    });
+    // A separate single-value "UF" table, mirroring the per-sort UF the real
+    // encoder self-loops into: (output output) -> Unit-ish value.
+    let uf_table = egraph.add_table(FunctionConfig {
+        schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Base(int_base)],
+        num_values: 1,
+        identity_values: None,
+        default: DefaultVal::Fail,
+        merge: MergeFn::Old,
+        name: "uf".into(),
+        can_subsume: false,
+    });
+    // The custom function f: (i64) -> Id. On a key collision its merge mints the
+    // view over (old, new) (self-looping the minted output into `uf`) and returns
+    // the minted output. Mirrors `fd_mint_to_mergefn`'s `Seq([TableInsert, mint])`.
+    let marker = egraph.base_values_mut().get(7i64);
+    let mint = || {
+        MergeFn::Construct(
+            view_table,
+            vec![MergeFn::Old, MergeFn::New],
+            vec![MergeFn::Const(marker)],
+        )
+    };
+    let f_table = egraph.add_table(FunctionConfig {
+        schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
+        default: DefaultVal::Fail,
+        merge: MergeFn::Seq(vec![
+            MergeFn::TableInsert(uf_table, vec![mint(), mint(), MergeFn::Const(marker)]),
+            mint(),
+        ]),
+        name: "f".into(),
+        can_subsume: false,
+    });
+
+    let key0 = egraph.base_values_mut().get(0i64);
+    let a = egraph.fresh_id();
+    let b = egraph.fresh_id();
+    // f(0) = a, then f(0) = b -> collision -> merge mints view(a, b).
+    egraph.add_values(vec![(f_table, vec![key0, a])]);
+    egraph.add_values(vec![(f_table, vec![key0, b])]);
+    egraph.flush_updates();
+
+    // The view should now have exactly one row keyed (a, b) with the marker in
+    // its second value column.
+    let mut rows = Vec::new();
+    egraph.for_each(view_table, |row| rows.push(row.vals.to_vec()));
+    assert_eq!(rows.len(), 1, "expected exactly one minted view row");
+    let row = &rows[0];
+    assert_eq!(row[0], a, "view key child a");
+    assert_eq!(row[1], b, "view key child b");
+    // row[2] is the minted output; row[3] is the extra value column.
+    assert_eq!(
+        row[3], marker,
+        "view extra value column should be the marker"
+    );
+}
+
+/// `FunctionConfig::identity_values = Some(k)` must short-circuit a merge whose
+/// leading `k` value columns are unchanged: the existing row is kept verbatim
+/// and the (side-effecting) merge body must NOT run. A collision that DOES
+/// change an identity column runs the body as usual. Mirrors the proof-encoding
+/// FD pair view `(children) -> (output, proof)` (`Some(1)`): an equal-output
+/// collision keeps the existing proof instead of re-running the proof-minting
+/// merge body.
+#[test]
+fn identity_column_short_circuit() {
+    let mut egraph = EGraph::default();
+    let int_base = egraph.base_values_mut().register_type::<i64>();
+
+    // A "log" table the passenger merge inserts into, so we can observe whether
+    // the (side-effecting) merge body actually ran. Key = the new passenger
+    // value; the row's mere existence is the signal.
+    let log_table = egraph.add_table(FunctionConfig {
+        schema: vec![ColumnTy::Base(int_base), ColumnTy::Base(int_base)],
+        num_values: 1,
+        identity_values: None,
+        default: DefaultVal::Fail,
+        merge: MergeFn::Old,
+        name: "log".into(),
+        can_subsume: false,
+    });
+    let marker = egraph.base_values_mut().get(1i64);
+
+    // The FD-style view: (key) -> (output, passenger). `identity_values: Some(1)`
+    // means only the output column matters. The passenger merge logs that it ran
+    // and keeps the new value; the output merge keeps `old`.
+    let view = egraph.add_table(FunctionConfig {
+        schema: vec![
+            ColumnTy::Base(int_base),
+            ColumnTy::Base(int_base), // output (identity)
+            ColumnTy::Base(int_base), // passenger
+        ],
+        num_values: 2,
+        identity_values: Some(1),
+        default: DefaultVal::Fail,
+        merge: MergeFn::Tuple(vec![
+            MergeFn::OldCol(0),
+            // Passenger merge: log that the body ran, then take the new value.
+            MergeFn::Seq(vec![
+                MergeFn::TableInsert(log_table, vec![MergeFn::NewCol(1), MergeFn::Const(marker)]),
+                MergeFn::NewCol(1),
+            ]),
+        ]),
+        name: "view".into(),
+        can_subsume: false,
+    });
+
+    let key = egraph.base_values_mut().get(0i64);
+    let out = egraph.base_values_mut().get(100i64);
+    let p1 = egraph.base_values_mut().get(10i64);
+    let p2 = egraph.base_values_mut().get(20i64);
+
+    // Equal-output collision: same output 100, different passenger (10 -> 20).
+    // The short-circuit must keep the existing row and NOT run the merge body,
+    // so the log stays empty and the passenger stays 10.
+    egraph.add_values(vec![(view, vec![key, out, p1])]);
+    egraph.add_values(vec![(view, vec![key, out, p2])]);
+    egraph.flush_updates();
+
+    let mut log_rows = 0usize;
+    egraph.for_each(log_table, |_| log_rows += 1);
+    assert_eq!(
+        log_rows, 0,
+        "equal-output collision must short-circuit (no merge-body side effect)"
+    );
+    let mut view_rows = Vec::new();
+    egraph.for_each(view, |row| view_rows.push(row.vals.to_vec()));
+    assert_eq!(view_rows.len(), 1);
+    assert_eq!(view_rows[0][1], out, "output kept");
+    assert_eq!(
+        view_rows[0][2], p1,
+        "passenger kept from the existing row (merge body did not run)"
+    );
+
+    // Differing-output collision: new output 200. The identity column changed,
+    // so the merge body MUST run (logging) and the output/passenger update per
+    // the merge (output keeps old=100, passenger logs and takes new=30).
+    let out2 = egraph.base_values_mut().get(200i64);
+    let p3 = egraph.base_values_mut().get(30i64);
+    egraph.add_values(vec![(view, vec![key, out2, p3])]);
+    egraph.flush_updates();
+
+    log_rows = 0;
+    egraph.for_each(log_table, |_| log_rows += 1);
+    assert_eq!(
+        log_rows, 1,
+        "differing-output collision must run the merge body (one log row)"
+    );
+}
+
 #[test]
 fn math() {
     let handles =
@@ -208,6 +391,8 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
     // tables
     let diff = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "diff".into(),
@@ -215,6 +400,8 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
     });
     let integral = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "integral".into(),
@@ -222,6 +409,8 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
     });
     let add = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "add".into(),
@@ -229,6 +418,8 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
     });
     let sub = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "sub".into(),
@@ -236,6 +427,8 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
     });
     let mul = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "mul".into(),
@@ -243,6 +436,8 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
     });
     let div = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "div".into(),
@@ -250,6 +445,8 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
     });
     let pow = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "pow".into(),
@@ -258,6 +455,8 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
 
     let ln = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "ln".into(),
@@ -265,6 +464,8 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
     });
     let sqrt = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "sqrt".into(),
@@ -272,6 +473,8 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
     });
     let sin = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "sin".into(),
@@ -279,6 +482,8 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
     });
     let cos = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "cos".into(),
@@ -286,6 +491,8 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
     });
     let rat = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(rational_ty), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "rat".into(),
@@ -293,6 +500,8 @@ fn math_test(mut egraph: EGraph, can_subsume: bool) {
     });
     let var = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(string_ty), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "var".into(),
@@ -535,6 +744,8 @@ fn container_test() {
     let int_base = egraph.base_values_mut().register_type::<i64>();
     let num_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "num".into(),
@@ -542,6 +753,8 @@ fn container_test() {
     });
     let add_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id; 3],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "add".into(),
@@ -549,6 +762,8 @@ fn container_test() {
     });
     let vec_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id; 2],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "vec".into(),
@@ -720,6 +935,8 @@ fn run_query_prim_container_match_case(seminaive: bool, seed_canonical: bool) ->
     let mut egraph = EGraph::default();
     let k_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "k".into(),
@@ -727,6 +944,8 @@ fn run_query_prim_container_match_case(seminaive: bool, seed_canonical: bool) ->
     });
     let w_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "w".into(),
@@ -734,6 +953,8 @@ fn run_query_prim_container_match_case(seminaive: bool, seed_canonical: bool) ->
     });
     let l_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "l".into(),
@@ -822,6 +1043,8 @@ fn rhs_only_rule() {
     let one = egraph.base_values_mut().get(1i64);
     let num_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "num".into(),
@@ -910,6 +1133,8 @@ fn mergefn_arithmetic() {
     // This uses nested MergeFn::Primitive with external functions to build the complex merge function
     let f_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(int_base), ColumnTy::Base(int_base)],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::Fail,
         merge: MergeFn::Primitive(
             add_func,
@@ -1006,6 +1231,8 @@ fn mergefn_nested_function() {
     // Create a function g that will be used in the merge function for f
     let g_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "g".into(),
@@ -1016,6 +1243,8 @@ fn mergefn_nested_function() {
     // This uses nested MergeFn::Function to build the complex merge function
     let f_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::Function(
             g_table,
@@ -1128,6 +1357,8 @@ fn constrain_prims_simple() {
     let bool_base = egraph.base_values_mut().register_type::<bool>();
     let f_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "f".into(),
@@ -1135,6 +1366,8 @@ fn constrain_prims_simple() {
     });
     let g_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "g".into(),
@@ -1221,6 +1454,8 @@ fn constrain_prims_abstract() {
     let int_base = egraph.base_values_mut().register_type::<i64>();
     let f_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "f".into(),
@@ -1228,6 +1463,8 @@ fn constrain_prims_abstract() {
     });
     let g_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "g".into(),
@@ -1318,6 +1555,8 @@ fn basic_subsumption() {
     let int_base = egraph.base_values_mut().register_type::<i64>();
     let f_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "f".into(),
@@ -1325,6 +1564,8 @@ fn basic_subsumption() {
     });
     let g_table = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::FreshId,
         merge: MergeFn::UnionId,
         name: "g".into(),
@@ -1397,6 +1638,8 @@ fn lookup_failure_panics() {
     let mut egraph = EGraph::default();
     let f = egraph.add_table(FunctionConfig {
         schema: vec![ColumnTy::Id, ColumnTy::Id],
+        num_values: 1,
+        identity_values: None,
         default: DefaultVal::Fail,
         merge: MergeFn::UnionId,
         name: "test".into(),
diff --git a/src/ast/desugar.rs b/src/ast/desugar.rs
index 11614aa73..81b3e08cc 100644
--- a/src/ast/desugar.rs
+++ b/src/ast/desugar.rs
@@ -16,15 +16,19 @@ pub(crate) fn desugar_command(
             name,
             schema,
             merge,
+            merge_action,
             hidden,
             let_binding,
             term_constructor,
+            identity_values,
             unextractable,
         } => {
             let mut fdecl = FunctionDecl::function(span, name, schema, merge);
+            fdecl.merge_action = merge_action;
             fdecl.internal_hidden = hidden;
             fdecl.internal_let = let_binding;
             fdecl.term_constructor = term_constructor;
+            fdecl.identity_values = identity_values;
             // Functions with term_constructor are view tables that should be
             // extractable unless explicitly marked unextractable
             if fdecl.term_constructor.is_some() {
diff --git a/src/ast/mod.rs b/src/ast/mod.rs
index 4d1126dce..79867f218 100644
--- a/src/ast/mod.rs
+++ b/src/ast/mod.rs
@@ -141,9 +141,11 @@ where
                     schema: f.schema.clone(),
                     name: f.name.clone(),
                     merge: f.merge.clone(),
+                    merge_action: f.merge_action.clone(),
                     hidden: f.internal_hidden,
                     let_binding: f.internal_let,
                     term_constructor: f.term_constructor.clone(),
+                    identity_values: f.identity_values,
                     unextractable: f.unextractable,
                 },
             },
@@ -700,9 +702,14 @@ where
         name: String,
         schema: Schema,
         merge: Option<GenericExpr<Head, Leaf>>,
+        /// Effect actions run before computing the merge value (block-form
+        /// `:merge`). Empty for the common single-expression merge.
+        merge_action: GenericActions<Head, Leaf>,
         hidden: bool,
         let_binding: bool,
         term_constructor: Option<String>,
+        /// Internal `:identity-values <n>` annotation (proof-encoding FD views).
+        identity_values: Option<usize>,
         unextractable: bool,
     },
 
@@ -979,14 +986,25 @@ where
                 name,
                 schema,
                 merge,
+                merge_action,
                 hidden,
                 let_binding,
                 term_constructor,
+                identity_values,
                 unextractable,
             } => {
                 write!(f, "(function {name} {schema}")?;
                 if let Some(merge) = &merge {
-                    write!(f, " :merge {merge}")?;
+                    if merge_action.0.is_empty() {
+                        write!(f, " :merge {merge}")?;
+                    } else {
+                        // block-form merge: an action sequence then the value
+                        write!(f, " :merge (")?;
+                        for action in &merge_action.0 {
+                            write!(f, "{action} ")?;
+                        }
+                        write!(f, "{merge})")?;
+                    }
                 } else {
                     write!(f, " :no-merge")?;
                 }
@@ -1002,6 +1020,9 @@ where
                 if let Some(tc) = term_constructor {
                     write!(f, " :internal-term-constructor {tc}")?;
                 }
+                if let Some(n) = identity_values {
+                    write!(f, " :identity-values {n}")?;
+                }
                 write!(f, ")")
             }
             GenericCommand::Constructor {
@@ -1250,6 +1271,9 @@ where
     /// Resolved schema after typechecking is stored here, otherwise "".
     pub resolved_schema: Head,
     pub merge: Option<GenericExpr<Head, Leaf>>,
+    /// Effect actions run before computing the merge value (block-form
+    /// `:merge`). Empty for the common single-expression merge.
+    pub merge_action: GenericActions<Head, Leaf>,
     pub cost: Option<DefaultCost>,
     pub unextractable: bool,
     /// Hidden functions are excluded from print-size output.
@@ -1262,6 +1286,12 @@ where
     /// For view tables in proof encoding: the constructor to use for building
     /// terms from the first n-1 children during extraction.
     pub term_constructor: Option<String>,
+    /// Internal annotation (`:identity-values <n>`) used only by proof-encoding
+    /// FD view tables. When `Some(k)`, a merge collision that leaves the leading
+    /// `k` value columns unchanged is treated as a no-op (the side-effecting
+    /// merge body is skipped). `None` (the default for all user functions) keeps
+    /// classic merge semantics: the merge body always runs.
+    pub identity_values: Option<usize>,
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
@@ -1318,12 +1348,14 @@ impl FunctionDecl {
             schema,
             resolved_schema: String::new(),
             merge,
+            merge_action: Default::default(),
             cost: None,
             unextractable: true,
             internal_hidden: false,
             internal_let: false,
             span,
             term_constructor: None,
+            identity_values: None,
         }
     }
 
@@ -1342,12 +1374,14 @@ impl FunctionDecl {
             resolved_schema: String::new(),
             schema,
             merge: None,
+            merge_action: Default::default(),
             cost,
             unextractable,
             internal_hidden: hidden,
             internal_let: false,
             span,
             term_constructor: None,
+            identity_values: None,
         }
     }
 }
@@ -1367,12 +1401,14 @@ where
             schema: self.schema,
             resolved_schema: self.resolved_schema,
             merge: self.merge.map(|expr| expr.visit_exprs(f)),
+            merge_action: self.merge_action.visit_exprs(f),
             cost: self.cost,
             unextractable: self.unextractable,
             internal_hidden: self.internal_hidden,
             internal_let: self.internal_let,
             span: self.span,
             term_constructor: self.term_constructor,
+            identity_values: self.identity_values,
         }
     }
 }
@@ -1692,9 +1728,11 @@ where
                 name,
                 schema,
                 merge,
+                merge_action,
                 hidden,
                 let_binding,
                 term_constructor,
+                identity_values,
                 unextractable,
             } => GenericCommand::Function {
                 span,
@@ -1704,9 +1742,11 @@ where
                     output: fun(schema.output),
                 },
                 merge,
+                merge_action,
                 hidden,
                 let_binding,
                 term_constructor: term_constructor.map(&mut *fun),
+                identity_values,
                 unextractable,
             },
             GenericCommand::AddRuleset(span, name) => GenericCommand::AddRuleset(span, fun(name)),
@@ -1786,18 +1826,22 @@ where
                 name,
                 schema,
                 merge,
+                merge_action,
                 hidden,
                 let_binding,
                 term_constructor,
+                identity_values,
                 unextractable,
             } => GenericCommand::Function {
                 span,
                 name,
                 schema,
                 merge: merge.map(|e| e.visit_exprs(f)),
+                merge_action: merge_action.visit_exprs(f),
                 hidden,
                 let_binding,
                 term_constructor,
+                identity_values,
                 unextractable,
             },
             GenericCommand::Rule { rule } => GenericCommand::Rule {
@@ -1925,18 +1969,22 @@ where
                 name,
                 schema,
                 merge,
+                merge_action,
                 hidden,
                 let_binding,
                 term_constructor,
+                identity_values,
                 unextractable,
             } => GenericCommand::Function {
                 span,
                 name,
                 schema,
                 merge: merge.map(|expr| expr.map_symbols(head, leaf)),
+                merge_action: merge_action.map_symbols(head, leaf),
                 hidden,
                 let_binding,
                 term_constructor,
+                identity_values,
                 unextractable,
             },
             GenericCommand::AddRuleset(span, name) => GenericCommand::AddRuleset(span, name),
diff --git a/src/ast/parse.rs b/src/ast/parse.rs
index 4d0aebb5e..0c25495a9 100644
--- a/src/ast/parse.rs
+++ b/src/ast/parse.rs
@@ -336,9 +336,11 @@ impl Parser {
             "function" => match tail {
                 [name, inputs, output, rest @ ..] => {
                     let mut merge = None;
+                    let mut merge_action = GenericActions(Vec::new());
                     let mut hidden = false;
                     let mut let_binding = false;
                     let mut term_constructor = None;
+                    let mut identity_values = None;
                     let mut unextractable = false;
                     for (key, val) in self.parse_options(rest)? {
                         match (key, val) {
@@ -358,7 +360,24 @@ impl Parser {
                                         "conflicting merge options: :merge and :no-merge cannot both be specified"
                                     );
                                 }
-                                merge = Some(Some(self.parse_expr(e)?));
+                                // Block form `:merge ((action)... value)`: when the
+                                // first element is itself a list, the leading forms are
+                                // effect actions and the last form is the merged value.
+                                // (A plain expression always has an atom head.)
+                                if let Sexp::List(items, _) = e
+                                    && let [Sexp::List(..), ..] = items.as_slice()
+                                {
+                                    let (value_sexp, action_sexps) =
+                                        items.split_last().expect("non-empty list");
+                                    let mut actions = Vec::new();
+                                    for a in action_sexps {
+                                        actions.extend(self.parse_action(a)?);
+                                    }
+                                    merge_action = GenericActions(actions);
+                                    merge = Some(Some(self.parse_expr(value_sexp)?));
+                                } else {
+                                    merge = Some(Some(self.parse_expr(e)?));
+                                }
                             }
                             (":internal-hidden", []) => hidden = true,
                             (":internal-let", []) => let_binding = true,
@@ -366,6 +385,10 @@ impl Parser {
                             (":internal-term-constructor", [tc]) => {
                                 term_constructor = Some(tc.expect_atom("term constructor name")?)
                             }
+                            (":identity-values", [n]) => {
+                                identity_values =
+                                    Some(n.expect_uint::<usize>("identity-values count")?)
+                            }
                             _ => return error!(span, "could not parse function options"),
                         }
                     }
@@ -382,9 +405,11 @@ impl Parser {
                         name: name.expect_atom("function name")?,
                         schema: self.parse_schema(inputs, output)?,
                         merge,
+                        merge_action,
                         hidden,
                         let_binding,
                         term_constructor,
+                        identity_values,
                         unextractable,
                         span,
                     }]
diff --git a/src/ast/proof_global_remover.rs b/src/ast/proof_global_remover.rs
index 2cbbb4b77..976804086 100644
--- a/src/ast/proof_global_remover.rs
+++ b/src/ast/proof_global_remover.rs
@@ -90,12 +90,14 @@ fn remove_globals_cmd(cmd: ResolvedNCommand) -> Vec<ResolvedNCommand> {
                     },
                     resolved_schema: resolved_call.clone(),
                     merge: None,
+                    merge_action: Default::default(),
                     cost: None,
                     unextractable: true,
                     internal_hidden: false,
                     internal_let: true,
                     span: span.clone(),
                     term_constructor: None,
+                    identity_values: None,
                 };
                 vec![
                     GenericNCommand::Function(func_decl),
diff --git a/src/ast/remove_globals.rs b/src/ast/remove_globals.rs
index c37f908af..154193cd5 100644
--- a/src/ast/remove_globals.rs
+++ b/src/ast/remove_globals.rs
@@ -108,12 +108,14 @@ impl GlobalRemover<'_> {
                         },
                         resolved_schema: resolved_call.clone(),
                         merge: None,
+                        merge_action: Default::default(),
                         cost: None,
                         unextractable: true,
                         internal_hidden: false,
                         internal_let: true,
                         span: span.clone(),
                         term_constructor: None,
+                        identity_values: None,
                     };
                     vec![
                         GenericNCommand::Function(func_decl),
diff --git a/src/extract.rs b/src/extract.rs
index e49fa2759..74cbd0e38 100644
--- a/src/extract.rs
+++ b/src/extract.rs
@@ -231,13 +231,14 @@ impl<C: Cost + Ord + Eq + Clone + Debug> Extractor<C> {
             {
                 let func_name = func.0.clone();
                 // For view tables (with term_constructor in proof mode), the e-class is the last input column
-                let output_sort_name = func.1.extraction_output_sort().name();
+                let output_sort = func.1.extraction_output_sort(egraph);
+                let output_sort_name = output_sort.name();
                 if let Some(v) = rev_index.get_mut(output_sort_name) {
                     v.push(func_name);
                 } else {
                     rev_index.insert(output_sort_name.to_owned(), vec![func_name]);
                     if extract_all_sorts {
-                        rootsorts.push(func.1.extraction_output_sort().clone());
+                        rootsorts.push(func.1.extraction_output_sort(egraph).clone());
                     }
                 }
             }
@@ -270,7 +271,7 @@ impl<C: Cost + Ord + Eq + Clone + Debug> Extractor<C> {
                     if !funcs_set.contains(h) {
                         let func = egraph.functions.get(h).unwrap();
                         // For view tables, children are all but the last input (which is the e-class)
-                        let num_children = func.extraction_num_children();
+                        let num_children = func.extraction_num_children(egraph);
                         for ch in func.schema.input.iter().take(num_children) {
                             let ch_name = ch.name();
                             if !seen.contains(ch_name) {
@@ -293,7 +294,8 @@ impl<C: Cost + Ord + Eq + Clone + Debug> Extractor<C> {
 
         for func_name in funcs.iter() {
             let func = egraph.functions.get(func_name).unwrap();
-            let output_sort_name = func.extraction_output_sort().name();
+            let output_sort = func.extraction_output_sort(egraph);
+            let output_sort_name = output_sort.name();
             if !costs.contains_key(output_sort_name) {
                 costs.insert(output_sort_name.to_owned(), Default::default());
                 topo_rnk.insert(output_sort_name.to_owned(), Default::default());
@@ -347,7 +349,7 @@ impl<C: Cost + Ord + Eq + Clone + Debug> Extractor<C> {
     ) -> Option<C> {
         let mut ch_costs: Vec<C> = Vec::new();
         let sorts = &func.schema.input;
-        let num_children = func.extraction_num_children();
+        let num_children = func.extraction_num_children(egraph);
         for (value, sort) in row.vals.iter().take(num_children).zip(sorts.iter()) {
             ch_costs.push(self.compute_cost_node(egraph, *value, sort)?);
         }
@@ -384,7 +386,7 @@ impl<C: Cost + Ord + Eq + Clone + Debug> Extractor<C> {
         func: &Function,
     ) -> usize {
         let sorts = &func.schema.input;
-        let num_children = func.extraction_num_children();
+        let num_children = func.extraction_num_children(egraph);
         row.vals
             .iter()
             .take(num_children)
@@ -414,9 +416,9 @@ impl<C: Cost + Ord + Eq + Clone + Debug> Extractor<C> {
 
             for func_name in funcs.iter() {
                 let func = egraph.functions.get(func_name).unwrap();
-                let target_sort = func.extraction_output_sort();
+                let target_sort = func.extraction_output_sort(egraph);
 
-                let output_idx = func.extraction_output_index();
+                let output_idx = func.extraction_output_index(egraph);
                 let relax_hyperedge = |row: egglog_bridge::FunctionRow| {
                     if !row.subsumed {
                         let target = &row.vals[output_idx];
@@ -461,8 +463,8 @@ impl<C: Cost + Ord + Eq + Clone + Debug> Extractor<C> {
         // Save the edges for reconstruction
         for func_name in funcs.iter() {
             let func = egraph.functions.get(func_name).unwrap();
-            let target_sort = func.extraction_output_sort();
-            let output_idx = func.extraction_output_index();
+            let target_sort = func.extraction_output_sort(egraph);
+            let output_idx = func.extraction_output_index(egraph);
 
             let save_best_parent_edge = |row: egglog_bridge::FunctionRow| {
                 if !row.subsumed {
@@ -547,7 +549,7 @@ impl<C: Cost + Ord + Eq + Clone + Debug> Extractor<C> {
             let func = egraph.functions.get(func_name).unwrap();
             let ch_sorts = &func.schema.input;
 
-            let num_children = func.extraction_num_children();
+            let num_children = func.extraction_num_children(egraph);
             let output_name = func.extraction_term_name();
 
             let mut ch_terms: Vec<TermId> = Vec::new();
@@ -673,7 +675,7 @@ impl<C: Cost + Ord + Eq + Clone + Debug> Extractor<C> {
                         .functions
                         .get(func_name)
                         .unwrap()
-                        .extraction_output_sort()
+                        .extraction_output_sort(egraph)
                         .name()
                 {
                     root_funcs.push(func_name.clone());
@@ -682,7 +684,7 @@ impl<C: Cost + Ord + Eq + Clone + Debug> Extractor<C> {
 
             for func_name in root_funcs.iter() {
                 let func = egraph.functions.get(func_name).unwrap();
-                let output_idx = func.extraction_output_index();
+                let output_idx = func.extraction_output_index(egraph);
 
                 let find_root_variants = |row: egglog_bridge::FunctionRow| {
                     if !row.subsumed {
@@ -705,7 +707,7 @@ impl<C: Cost + Ord + Eq + Clone + Debug> Extractor<C> {
                 let mut ch_terms: Vec<TermId> = Vec::new();
                 let func = egraph.functions.get(&func_name).unwrap();
                 let ch_sorts = &func.schema.input;
-                let num_children = func.extraction_num_children();
+                let num_children = func.extraction_num_children(egraph);
                 // For view tables, children are all but the last input (which is the e-class)
                 for (value, sort) in hyperedge.iter().zip(ch_sorts.iter()).take(num_children) {
                     ch_terms.push(self.reconstruct_termdag_node_helper(
@@ -771,21 +773,48 @@ impl Function {
         }
     }
 
-    /// For view tables (with term_constructor), the effective output sort is the last input column.
-    /// For regular tables, it's the output sort.
-    /// This is used by extraction to determine which sort a table produces values for.
-    pub(crate) fn extraction_output_sort(&self) -> &ArcSort {
-        if self.decl.term_constructor.is_some() {
-            self.schema.input.last().unwrap()
+    /// Whether this is a "legacy" view table whose e-class lives in the last input
+    /// column (the old custom-function view shape). FD views — whose `term_constructor`
+    /// is a constructor or a primitive-bodied custom — keep the output in the value
+    /// column and behave like a regular table for extraction.
+    fn is_legacy_view(&self, egraph: &EGraph) -> bool {
+        match &self.decl.term_constructor {
+            Some(tc) => {
+                // FD views (constructors + primitive-bodied customs recorded by the
+                // proof encoder) are not legacy.
+                if egraph.proof_state.fd_view_funcs.contains(tc) {
+                    return false;
+                }
+                egraph
+                    .functions
+                    .get(tc)
+                    .map(|f| f.decl.subtype != FunctionSubtype::Constructor)
+                    .unwrap_or(false)
+            }
+            None => false,
+        }
+    }
+
+    /// The sort this table produces values for during extraction.
+    /// For legacy view tables this is the last input column (the e-class);
+    /// otherwise it is the output sort.
+    pub(crate) fn extraction_output_sort(&self, egraph: &EGraph) -> ArcSort {
+        if self.is_legacy_view(egraph) {
+            self.schema.input.last().unwrap().clone()
+        } else if let Some((first, _second)) = EGraph::pair_components(&self.schema.output) {
+            // A pair-valued FD view stores `[children..., output, proof]`; the
+            // extracted value (at `extraction_output_index`) is the output, so
+            // its sort is the pair's first component, not the pair sort itself.
+            first
         } else {
-            &self.schema.output
+            self.schema.output.clone()
         }
     }
 
     /// Returns the number of children for extraction purposes.
-    /// For view tables, this excludes the last column (the e-class).
-    pub(crate) fn extraction_num_children(&self) -> usize {
-        if self.decl.term_constructor.is_some() {
+    /// For legacy view tables, this excludes the last input (the e-class).
+    pub(crate) fn extraction_num_children(&self, egraph: &EGraph) -> usize {
+        if self.is_legacy_view(egraph) {
             self.schema.input.len() - 1
         } else {
             self.schema.input.len()
@@ -802,16 +831,14 @@ impl Function {
     }
 
     /// Returns the index of the output value in a row for extraction purposes.
-    /// For view tables, the e-class is the last input column (second-to-last in the row).
-    /// For regular tables, it's the last column (the actual output).
-    pub(crate) fn extraction_output_index(&self) -> usize {
-        if self.decl.term_constructor.is_some() {
-            // For view tables: input is [children..., eclass], output is view_sort
-            // Row is [children..., eclass, view_sort]
-            // We want eclass which is at index input.len() - 1
+    /// For legacy view tables the e-class is the last input column; otherwise
+    /// it is the last column (the actual output).
+    pub(crate) fn extraction_output_index(&self, egraph: &EGraph) -> usize {
+        if self.is_legacy_view(egraph) {
+            // Legacy view: row is [children..., eclass, view_sort]; eclass at input.len() - 1.
             self.schema.input.len() - 1
         } else {
-            // For regular tables: row is [inputs..., output]
+            // Regular / FD view: row is [inputs..., output].
             self.schema.input.len()
         }
     }
diff --git a/src/lib.rs b/src/lib.rs
index c532beb28..b04790738 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -46,7 +46,7 @@ use csv::Writer;
 pub use egglog_add_primitive::add_literal_prim;
 pub use egglog_add_primitive::add_primitive;
 pub use egglog_add_primitive::add_primitive_with_validator;
-use egglog_ast::generic_ast::{Change, GenericExpr, Literal};
+use egglog_ast::generic_ast::{Change, GenericAction, GenericExpr, Literal};
 use egglog_ast::span::Span;
 use egglog_ast::util::ListDisplay;
 pub use egglog_bridge::FunctionRow;
@@ -482,6 +482,27 @@ impl Default for EGraph {
             if a > b { a } else { b }
         });
 
+        // `(select-eq a b x y)` returns `x` if `a == b` else `y`. Used in
+        // the FD-merge proof encoding to pick the orientation-correct proof
+        // (since a `:merge` expression cannot branch on `ordering-max`).
+        eg.add_pure_primitive(
+            SelectEq {
+                name: "select-eq".to_string(),
+            },
+            None,
+        );
+
+        // `(fd-mint (C children...) proof)` mints the pair-valued FD constructor `C`
+        // inside a `:merge` and returns C's output e-class. Only appears in encoder-
+        // generated merges; the lowering intercepts it (so its runtime `apply` is
+        // never reached) and the proof is written into C's view proof column.
+        eg.add_pure_primitive(
+            FdMint {
+                name: "fd-mint".to_string(),
+            },
+            None,
+        );
+
         eg.rulesets
             .insert("".into(), Ruleset::Rules(Default::default()));
 
@@ -489,6 +510,137 @@ impl Default for EGraph {
     }
 }
 
+/// `select-eq` primitive: `(select-eq a b x y)` returns `x` if `a == b`
+/// (value equality) else `y`.
+#[derive(Clone)]
+struct SelectEq {
+    name: String,
+}
+
+impl Primitive for SelectEq {
+    fn name(&self) -> &str {
+        &self.name
+    }
+
+    fn get_type_constraints(&self, span: &Span) -> Box<dyn TypeConstraint> {
+        Box::new(SelectEqTypeConstraint {
+            name: self.name.clone(),
+            span: span.clone(),
+        })
+    }
+}
+
+impl PurePrim for SelectEq {
+    fn apply<'a, 'db>(&self, _state: PureState<'a, 'db>, args: &[Value]) -> Option<Value> {
+        if args[0] == args[1] {
+            Some(args[2])
+        } else {
+            Some(args[3])
+        }
+    }
+}
+
+/// Type constraint for `select-eq`: `[a, b, x, y, output]` with `a==b` the
+/// same sort and `x==y==output` the same sort.
+struct SelectEqTypeConstraint {
+    name: String,
+    span: Span,
+}
+
+impl TypeConstraint for SelectEqTypeConstraint {
+    fn get(
+        &self,
+        arguments: &[AtomTerm],
+        _typeinfo: &TypeInfo,
+    ) -> Vec<Box<dyn Constraint<AtomTerm, ArcSort>>> {
+        // `[a, b, x, y, output]`
+        if arguments.len() != 5 {
+            return vec![constraint::impossible(
+                constraint::ImpossibleConstraint::ArityMismatch {
+                    atom: Atom {
+                        span: self.span.clone(),
+                        head: self.name.clone(),
+                        args: arguments.to_vec(),
+                    },
+                    expected: 5,
+                },
+            )];
+        }
+        vec![
+            constraint::eq(arguments[0].clone(), arguments[1].clone()),
+            constraint::eq(arguments[2].clone(), arguments[3].clone()),
+            constraint::eq(arguments[3].clone(), arguments[4].clone()),
+        ]
+    }
+}
+
+/// `fd-mint` primitive: `(fd-mint (C children...) proof)` mints the pair-valued
+/// FD constructor `C` inside a merge and returns its output e-class. See the
+/// registration site in `EGraph::default` for the full contract.
+#[derive(Clone)]
+struct FdMint {
+    name: String,
+}
+
+impl Primitive for FdMint {
+    fn name(&self) -> &str {
+        &self.name
+    }
+
+    fn get_type_constraints(&self, span: &Span) -> Box<dyn TypeConstraint> {
+        Box::new(FdMintTypeConstraint {
+            name: self.name.clone(),
+            span: span.clone(),
+        })
+    }
+}
+
+impl PurePrim for FdMint {
+    fn apply<'a, 'db>(&self, _state: PureState<'a, 'db>, args: &[Value]) -> Option<Value> {
+        // Never reached during normal evaluation (lowering intercepts it). If it
+        // were, the constructed value is the first argument.
+        Some(args[0])
+    }
+}
+
+/// Type constraint for `fd-mint`: `[constructed, proof, output]` with
+/// `constructed == output` (the result is C's output sort). The proof argument's
+/// sort is left free (it is the generated proof datatype).
+struct FdMintTypeConstraint {
+    name: String,
+    span: Span,
+}
+
+impl TypeConstraint for FdMintTypeConstraint {
+    fn get(
+        &self,
+        arguments: &[AtomTerm],
+        _typeinfo: &TypeInfo,
+    ) -> Vec<Box<dyn Constraint<AtomTerm, ArcSort>>> {
+        // `[viewname:String, constructed, proof?, output]`. The first argument is the
+        // FD view's name (a string literal), then the constructor application, then
+        // (proof mode only) the proof; the result sort equals the constructed value's
+        // sort (arg 1 == last). Arity 3 (term mode) or 4 (proof mode).
+        if arguments.len() != 3 && arguments.len() != 4 {
+            return vec![constraint::impossible(
+                constraint::ImpossibleConstraint::ArityMismatch {
+                    atom: Atom {
+                        span: self.span.clone(),
+                        head: self.name.clone(),
+                        args: arguments.to_vec(),
+                    },
+                    expected: 4,
+                },
+            )];
+        }
+        let last = arguments.len() - 1;
+        vec![
+            constraint::assign(arguments[0].clone(), StringSort.to_arcsort()),
+            constraint::eq(arguments[1].clone(), arguments[last].clone()),
+        ]
+    }
+}
+
 struct ResolvedNCommands {
     desugared: Vec<ResolvedNCommand>,
     /// In proof mode, populated with the desugared program before instrumented with proofs
@@ -749,6 +901,111 @@ impl EGraph {
         }
     }
 
+    /// Lower a `(fd-mint (C children...) [proof])` form into a `MergeFn` that mints
+    /// `C`'s e-class and returns it for use as a child of the merged value.
+    ///
+    /// The term constructor `C` (a `FreshId` default) mints the e-class; the view row,
+    /// per-sort UF self-loop, and `term_proof` are written as side effects so the
+    /// e-class is registered exactly as `add_term_and_view` would.
+    ///
+    /// `pair_mode` selects how sub-arguments are lowered: pair-scalar projections in
+    /// proof mode (where the merge value is a pair), plain expressions in term mode.
+    fn fd_mint_to_mergefn(
+        &self,
+        args: &[ResolvedExpr],
+        pair_mode: bool,
+    ) -> Result<egglog_bridge::MergeFn, Error> {
+        use egglog_bridge::MergeFn;
+        // `(fd-mint "viewname" (C children...) [proof])`.
+        let GenericExpr::Lit(_, Literal::String(view_name)) = &args[0] else {
+            return Err(Error::BackendError(
+                "fd-mint's first argument must be the FD view name (a string literal)".into(),
+            ));
+        };
+        let GenericExpr::Call(_, ResolvedCall::Func(c), child_args) = &args[1] else {
+            return Err(Error::BackendError(
+                "fd-mint's second argument must be a constructor application".into(),
+            ));
+        };
+        // The view table is named by the string literal, so this is self-contained
+        // on re-parse; it records the children->output row that all lookups consult.
+        let term_backend_id = self
+            .functions
+            .get(&c.name)
+            .ok_or_else(|| {
+                Error::BackendError(format!("fd-mint: constructor `{}` not declared", c.name))
+            })?
+            .backend_id;
+        let view_backend_id = self
+            .functions
+            .get(view_name.as_str())
+            .ok_or_else(|| {
+                Error::BackendError(format!("fd-mint: FD view `{view_name}` not declared"))
+            })?
+            .backend_id;
+        let lower = |a: &ResolvedExpr| {
+            if pair_mode {
+                self.translate_pair_scalar_to_mergefn(a)
+            } else {
+                self.translate_expr_to_mergefn(a)
+            }
+        };
+        let key = child_args
+            .iter()
+            .map(lower)
+            .collect::<Result<Vec<_>, _>>()?;
+        // Extra value columns written into the view besides the minted output: the
+        // proof in proof mode (`(fd-mint "v" (C ..) proof)`), none in term mode.
+        let value_args = args[2..].iter().map(lower).collect::<Result<Vec<_>, _>>()?;
+        // The minted e-class. `Function` runs the constructor's lookup_or_insert,
+        // idempotent per children, so we can re-evaluate it for each use.
+        let minted = || MergeFn::Function(term_backend_id, key.clone());
+        // The view row: key children, then the minted output, then any extra columns.
+        let mut view_row = key.clone();
+        view_row.push(minted());
+        view_row.extend(value_args.iter().cloned());
+        // Replicate the per-sort UF self-loop a normal constructor would write
+        // (`add_term_and_view`'s `(union out out proof)`), read during rebuild to
+        // canonicalize children. The proof is the view's existence proof, or Unit.
+        let uf_table = self
+            .proof_state
+            .uf_parent
+            .get(c.output.name())
+            .and_then(|uf_name| self.functions.get(uf_name))
+            .map(|f| f.backend_id);
+        let self_loop_proof = match value_args.last() {
+            Some(p) => p.clone(),
+            None => MergeFn::Const(self.backend.base_values().get(())),
+        };
+        let mut effects = vec![MergeFn::TableInsert(view_backend_id, view_row)];
+        if let Some(uf_backend_id) = uf_table {
+            effects.push(MergeFn::TableInsert(
+                uf_backend_id,
+                vec![minted(), minted(), self_loop_proof.clone()],
+            ));
+        }
+        // In proof mode, replicate `add_term_and_view`'s `term_proof(output) = proof`
+        // record so the minted e-class is queryable (only eq-sort outputs have a
+        // `term_proof` table, and only proof mode has a proof to store).
+        //
+        // Source the table from `proof_func_parent` (the sort's `:internal-proof-func`),
+        // not `proof_names.term_proof_name`: the former is re-populated on every parse
+        // (surviving the desugar-then-rerun round-trip); both name the same table.
+        if !value_args.is_empty()
+            && let Some(tp_name) = self.proof_state.proof_func_parent.get(c.output.name())
+            && let Some(tp) = self.functions.get(tp_name)
+        {
+            effects.push(MergeFn::TableInsert(
+                tp.backend_id,
+                vec![minted(), self_loop_proof],
+            ));
+        }
+        // Run the effects (write view row + UF self-loop + term_proof), then return
+        // the minted e-class.
+        effects.push(minted());
+        Ok(MergeFn::Seq(effects))
+    }
+
     fn translate_expr_to_mergefn(
         &self,
         expr: &ResolvedExpr,
@@ -775,6 +1032,12 @@ impl EGraph {
                 ))
             }
             GenericExpr::Call(_, ResolvedCall::Primitive(p), args) => {
+                // Term-mode constructor minting inside an FD merge: mint into the
+                // view (a plain `(C a b)` call would create the term but not the
+                // view row that lookups consult).
+                if p.name() == "fd-mint" {
+                    return self.fd_mint_to_mergefn(args, false);
+                }
                 let mut translated_args = args
                     .iter()
                     .map(|arg| self.translate_expr_to_mergefn(arg))
@@ -808,6 +1071,202 @@ impl EGraph {
         }
     }
 
+    /// Lower a (possibly block-form) merge into a backend [`MergeFn`].
+    ///
+    /// With no leading effect actions this is just the value expression. With
+    /// effect actions it becomes a `Seq` of the lowered actions followed by the
+    /// value, so the effects run (and declare their write-dependencies via
+    /// `TableInsert`) before the merged value is produced.
+    fn translate_merge_to_mergefn(
+        &self,
+        actions: &crate::ast::ResolvedActions,
+        value: &ResolvedExpr,
+    ) -> Result<egglog_bridge::MergeFn, Error> {
+        if actions.0.is_empty() {
+            return self.translate_expr_to_mergefn(value);
+        }
+        let mut items = Vec::with_capacity(actions.0.len() + 1);
+        for action in &actions.0 {
+            items.push(self.translate_action_to_mergefn(action)?);
+        }
+        items.push(self.translate_expr_to_mergefn(value)?);
+        Ok(egglog_bridge::MergeFn::Seq(items))
+    }
+
+    /// Lower a single effect action from a block-form merge. Only `(set (f
+    /// ...) v)` on a function is supported (it becomes a `TableInsert`, which
+    /// declares `f`'s table as a write-dependency of this merge).
+    fn translate_action_to_mergefn(
+        &self,
+        action: &crate::ast::ResolvedAction,
+    ) -> Result<egglog_bridge::MergeFn, Error> {
+        match action {
+            GenericAction::Set(_, ResolvedCall::Func(f), args, rhs) => {
+                let mut row = args
+                    .iter()
+                    .map(|arg| self.translate_expr_to_mergefn(arg))
+                    .collect::<Result<Vec<_>, _>>()?;
+                row.push(self.translate_expr_to_mergefn(rhs)?);
+                Ok(egglog_bridge::MergeFn::TableInsert(
+                    self.functions[&f.name].backend_id,
+                    row,
+                ))
+            }
+            _ => Err(Error::BackendError(
+                "only `(set (f ...) v)` actions are supported inside a `:merge` block".into(),
+            )),
+        }
+    }
+
+    /// Lower a (possibly block-form) merge for a pair-valued function. The merge
+    /// is written over boxed pairs, but the backend stores two value columns, so
+    /// `(pair a b)` becomes a top-level `Tuple` and `pair-first/second old/new`
+    /// map to the corresponding `OldCol`/`NewCol`.
+    fn translate_pair_merge_to_mergefn(
+        &self,
+        actions: &crate::ast::ResolvedActions,
+        value: &ResolvedExpr,
+    ) -> Result<egglog_bridge::MergeFn, Error> {
+        use egglog_bridge::MergeFn;
+        // The merged value is two columns, so the top-level merge must be a
+        // `Tuple` (the backend only special-cases a top-level `Tuple`):
+        let (mut col0, col1) = self.translate_pair_value_cols(value)?;
+        if !actions.0.is_empty() {
+            // Run the block's effect actions (e.g. the UF `set`) exactly once,
+            // as a prelude to computing column 0, by wrapping it in a `Seq`
+            // that returns the column-0 value after the effects.
+            let mut items = Vec::with_capacity(actions.0.len() + 1);
+            for action in &actions.0 {
+                items.push(self.translate_pair_action_to_mergefn(action)?);
+            }
+            items.push(col0);
+            col0 = MergeFn::Seq(items);
+        }
+        Ok(MergeFn::Tuple(vec![col0, col1]))
+    }
+
+    /// Lower a pair-typed merge value expression into its two per-column
+    /// merges `(col0, col1)`.
+    fn translate_pair_value_cols(
+        &self,
+        value: &ResolvedExpr,
+    ) -> Result<(egglog_bridge::MergeFn, egglog_bridge::MergeFn), Error> {
+        use egglog_bridge::MergeFn;
+        match value {
+            GenericExpr::Var(_, v) if v.name.as_str() == "old" => {
+                Ok((MergeFn::OldCol(0), MergeFn::OldCol(1)))
+            }
+            GenericExpr::Var(_, v) if v.name.as_str() == "new" => {
+                Ok((MergeFn::NewCol(0), MergeFn::NewCol(1)))
+            }
+            GenericExpr::Call(_, ResolvedCall::Primitive(p), args) if p.name() == "pair" => {
+                let a = self.translate_pair_scalar_to_mergefn(&args[0])?;
+                let b = self.translate_pair_scalar_to_mergefn(&args[1])?;
+                Ok((a, b))
+            }
+            _ => Err(Error::BackendError(
+                "the value of a `:merge` on a Pair-valued function must be `old`, `new`, \
+                 or a `(pair a b)` expression"
+                    .into(),
+            )),
+        }
+    }
+
+    /// Lower a scalar (single-column) sub-expression of a pair-valued merge.
+    /// `(pair-first old)`/`(pair-second old)` (and `new`) become column reads;
+    /// everything else recurses generically.
+    fn translate_pair_scalar_to_mergefn(
+        &self,
+        expr: &ResolvedExpr,
+    ) -> Result<egglog_bridge::MergeFn, Error> {
+        use egglog_bridge::MergeFn;
+        if let GenericExpr::Call(_, ResolvedCall::Primitive(p), args) = expr {
+            let proj = match p.name() {
+                "pair-first" => Some(0usize),
+                "pair-second" => Some(1usize),
+                _ => None,
+            };
+            if let (Some(col), GenericExpr::Var(_, v)) = (proj, &args[0]) {
+                match v.name.as_str() {
+                    "old" => return Ok(MergeFn::OldCol(col)),
+                    "new" => return Ok(MergeFn::NewCol(col)),
+                    _ => {}
+                }
+            }
+            if p.name() == "fd-mint" {
+                return self.fd_mint_to_mergefn(args, true);
+            }
+        }
+        match expr {
+            GenericExpr::Lit(_, literal) => {
+                Ok(MergeFn::Const(literal_to_value(&self.backend, literal)))
+            }
+            GenericExpr::Var(span, v) => {
+                // A bare `old`/`new` here would be a pair used as a scalar,
+                // which is unsupported; other vars are unbound.
+                Err(TypeError::Unbound(v.name.clone(), span.clone()).into())
+            }
+            GenericExpr::Call(_, ResolvedCall::Func(f), args) => {
+                let translated = args
+                    .iter()
+                    .map(|a| self.translate_pair_scalar_to_mergefn(a))
+                    .collect::<Result<Vec<_>, _>>()?;
+                Ok(MergeFn::Function(
+                    self.functions[&f.name].backend_id,
+                    translated,
+                ))
+            }
+            GenericExpr::Call(_, ResolvedCall::Primitive(p), args) => {
+                let translated = args
+                    .iter()
+                    .map(|a| self.translate_pair_scalar_to_mergefn(a))
+                    .collect::<Result<Vec<_>, _>>()?;
+                Ok(MergeFn::Primitive(
+                    p.external_id(crate::Context::Write),
+                    translated,
+                ))
+            }
+        }
+    }
+
+    /// Lower a single effect action inside a pair-valued merge block. Only
+    /// `(set (f ...) v)` is supported; its arguments are scalar projections.
+    fn translate_pair_action_to_mergefn(
+        &self,
+        action: &crate::ast::ResolvedAction,
+    ) -> Result<egglog_bridge::MergeFn, Error> {
+        match action {
+            GenericAction::Set(_, ResolvedCall::Func(f), args, rhs) => {
+                let mut row = args
+                    .iter()
+                    .map(|arg| self.translate_pair_scalar_to_mergefn(arg))
+                    .collect::<Result<Vec<_>, _>>()?;
+                row.push(self.translate_pair_scalar_to_mergefn(rhs)?);
+                Ok(egglog_bridge::MergeFn::TableInsert(
+                    self.functions[&f.name].backend_id,
+                    row,
+                ))
+            }
+            _ => Err(Error::BackendError(
+                "only `(set (f ...) v)` actions are supported inside a `:merge` block".into(),
+            )),
+        }
+    }
+
+    /// If `sort` is a `Pair` container sort, return its two component sorts.
+    /// A function whose output is a `Pair` is stored with TWO value columns
+    /// (one per component) instead of a single boxed container value.
+    pub(crate) fn pair_components(sort: &ArcSort) -> Option<(ArcSort, ArcSort)> {
+        // A `PairSort` is wrapped in a `ContainerSortImpl<PairSort>` when turned
+        // into an `ArcSort`, so downcast to the wrapper and read its inner sort.
+        let pair = sort
+            .clone()
+            .as_arc_any()
+            .downcast::<crate::prelude::ContainerSortImpl<PairSort>>()
+            .ok()?;
+        Some((pair.0.first(), pair.0.second()))
+    }
+
     fn declare_function(&mut self, decl: &ResolvedFunctionDecl) -> Result<(), Error> {
         let get_sort = |name: &String| match self.type_info.get_sort_by_name(name) {
             Some(sort) => Ok(sort.clone()),
@@ -832,22 +1291,61 @@ impl EGraph {
         };
 
         use egglog_bridge::{DefaultVal, MergeFn};
+        // Multi-value output: a function whose output sort is a `Pair`
+        // container is stored as TWO value columns (its component sorts)
+        // instead of one boxed container value.
+        let pair_output = Self::pair_components(&output);
+        let (num_values, value_col_sorts): (usize, Vec<&ArcSort>) = match &pair_output {
+            Some((first, second)) => (2, vec![first, second]),
+            None => (1, vec![&output]),
+        };
         let backend_id = self.backend.add_table(egglog_bridge::FunctionConfig {
+            num_values,
+            // Identity-column merge short-circuit, opted into only by proof-encoding
+            // FD views via the internal `:identity-values <n>` annotation: when
+            // `Some(k)`, a collision leaving the leading `k` value columns unchanged
+            // skips the merge body. User functions keep `None` (classic semantics).
+            identity_values: decl.identity_values,
             schema: input
                 .iter()
-                .chain([&output])
+                .chain(value_col_sorts)
                 .map(|sort| sort.column_ty(&self.backend))
                 .collect(),
             default: match decl.subtype {
                 FunctionSubtype::Constructor => DefaultVal::FreshId,
                 FunctionSubtype::Custom => DefaultVal::Fail,
             },
-            merge: match decl.subtype {
-                FunctionSubtype::Constructor => MergeFn::UnionId,
-                FunctionSubtype::Custom => match &decl.merge {
-                    None => MergeFn::AssertEq,
-                    Some(expr) => self.translate_expr_to_mergefn(expr)?,
-                },
+            merge: {
+                // For the default merges (UnionId / AssertEq) a multi-value
+                // function applies the same per-column merge to each value
+                // column via a `Tuple`. Custom merges build their own
+                // (possibly tuple) merge in `translate_merge_to_mergefn`.
+                let default_multi = |mk: fn() -> MergeFn| -> MergeFn {
+                    if num_values == 1 {
+                        mk()
+                    } else {
+                        MergeFn::Tuple((0..num_values).map(|_| mk()).collect())
+                    }
+                };
+                match decl.subtype {
+                    FunctionSubtype::Constructor => default_multi(|| MergeFn::UnionId),
+                    FunctionSubtype::Custom => match &decl.merge {
+                        None => default_multi(|| MergeFn::AssertEq),
+                        Some(expr) => {
+                            if pair_output.is_some() {
+                                // Pair-valued function: the merge is written
+                                // over boxed pairs (`old`/`new`/`pair`/
+                                // `pair-first`/`pair-second`) but the backend
+                                // stores two columns, so lower it pair-aware
+                                // (the value becomes a `Tuple` of per-column
+                                // merges).
+                                self.translate_pair_merge_to_mergefn(&decl.merge_action, expr)?
+                            } else {
+                                self.translate_merge_to_mergefn(&decl.merge_action, expr)?
+                            }
+                        }
+                    },
+                }
             },
             name: decl.name.to_string(),
             can_subsume,
@@ -2420,9 +2918,25 @@ fn resolve_function_container_target_with_context(
     })
 }
 
+/// The two value-column entries bound for a pair-valued function call's
+/// result, plus the component sorts (for lazily boxing on a wholesale use).
+#[derive(Clone)]
+struct PairProjection {
+    col0: QueryEntry,
+    col1: QueryEntry,
+    first: ArcSort,
+    second: ArcSort,
+    pair_sort: ArcSort,
+}
+
 struct BackendRule<'a> {
     rb: egglog_bridge::RuleBuilder<'a>,
     entries: HashMap<core::ResolvedAtomTerm, QueryEntry>,
+    /// For a query result var of a pair-valued function, the two value-column
+    /// entries it was bound to. Lets `pair-first`/`pair-second` of such a var
+    /// fuse to a direct column read (no box/unbox roundtrip) — important for
+    /// the rebuild rules, which canonicalize the output column.
+    pair_projections: HashMap<core::ResolvedAtomTerm, PairProjection>,
     functions: &'a IndexMap<String, Function>,
     type_info: &'a TypeInfo,
     /// Whether primitives may read the database. When true the per-phase
@@ -2445,6 +2959,7 @@ impl<'a> BackendRule<'a> {
             type_info,
             requires_read_context,
             entries: Default::default(),
+            pair_projections: Default::default(),
         }
     }
 
@@ -2476,6 +2991,23 @@ impl<'a> BackendRule<'a> {
     }
 
     fn entry(&mut self, x: &core::ResolvedAtomTerm) -> QueryEntry {
+        if let Some(existing) = self.entries.get(x) {
+            return existing.clone();
+        }
+        // A wholesale use of a pair-valued function result: lazily box its two
+        // value columns into a pair value (projections are fused elsewhere, so
+        // this only fires when the whole pair is actually needed).
+        if let Some(proj) = self.pair_projections.get(x).cloned() {
+            let boxed = self.box_pair_query_value(
+                proj.col0,
+                proj.col1,
+                &proj.first,
+                &proj.second,
+                &proj.pair_sort,
+            );
+            self.entries.insert(x.clone(), boxed.clone());
+            return boxed;
+        }
         self.entries
             .entry(x.clone())
             .or_insert_with(|| match x {
@@ -2494,6 +3026,109 @@ impl<'a> BackendRule<'a> {
         self.functions[&f.name].backend_id
     }
 
+    /// If function `f`'s output sort is a `Pair` container, return
+    /// `(first_sort, second_sort, pair_sort)`. Such functions are stored with
+    /// two value columns; reads box the two columns back into a pair value and
+    /// writes unbox a pair value into the two columns.
+    fn pair_info(&self, f: &typechecking::FuncType) -> Option<(ArcSort, ArcSort, ArcSort)> {
+        let out = &f.output;
+        EGraph::pair_components(out).map(|(a, b)| (a, b, out.clone()))
+    }
+
+    /// Resolve a specialized `pair` family primitive (`pair` / `pair-first` /
+    /// `pair-second`) and return its external function id for `ctx`.
+    /// `in_sorts` are the argument sorts and `out_sort` is the result sort.
+    fn pair_prim_extid(
+        &self,
+        name: &str,
+        in_sorts: &[ArcSort],
+        out_sort: &ArcSort,
+        ctx: crate::Context,
+    ) -> ExternalFunctionId {
+        let mut types: Vec<ArcSort> = in_sorts.to_vec();
+        types.push(out_sort.clone());
+        match ResolvedCall::from_resolution(name, &types, self.type_info, ctx) {
+            ResolvedCall::Primitive(p) => p.external_id(ctx),
+            ResolvedCall::Func(_) => panic!("expected primitive resolution for {name}"),
+        }
+    }
+
+    /// Box two value-column entries into a fresh pair value on the query side
+    /// (via the `pair` primitive) and return the bound pair entry.
+    fn box_pair_query_value(
+        &mut self,
+        v0: QueryEntry,
+        v1: QueryEntry,
+        first: &ArcSort,
+        second: &ArcSort,
+        pair_sort: &ArcSort,
+    ) -> QueryEntry {
+        let ctx = self.query_context();
+        let ext = self.pair_prim_extid("pair", &[first.clone(), second.clone()], pair_sort, ctx);
+        let ty = pair_sort.column_ty(self.rb.egraph());
+        let result: QueryEntry = self.rb.new_var(ty).into();
+        self.rb
+            .query_prim(ext, &[v0, v1, result.clone()], ty)
+            .unwrap();
+        result
+    }
+
+    /// Unbox a `pair` value into its two component entries on the action side.
+    fn unbox_pair_action(
+        &mut self,
+        pair_val: QueryEntry,
+        first: &ArcSort,
+        second: &ArcSort,
+        pair_sort: &ArcSort,
+    ) -> (QueryEntry, QueryEntry) {
+        let ctx = self.action_context();
+        let first_ext =
+            self.pair_prim_extid("pair-first", std::slice::from_ref(pair_sort), first, ctx);
+        let second_ext =
+            self.pair_prim_extid("pair-second", std::slice::from_ref(pair_sort), second, ctx);
+        let v0 = self
+            .rb
+            .call_external_func(
+                first_ext,
+                std::slice::from_ref(&pair_val),
+                first.column_ty(self.rb.egraph()),
+                || "pair-first failed".to_string(),
+            )
+            .into();
+        let v1 = self
+            .rb
+            .call_external_func(
+                second_ext,
+                &[pair_val],
+                second.column_ty(self.rb.egraph()),
+                || "pair-second failed".to_string(),
+            )
+            .into();
+        (v0, v1)
+    }
+
+    /// If `prim` applied to `atom_args` is `pair-first`/`pair-second` of a
+    /// pair-valued function result that was recorded in `pair_projections`,
+    /// return `(value_col_index, projection, result_term)`. The primitive's
+    /// atom args are `[pair_arg, result]`.
+    fn pair_projection_fusion(
+        &self,
+        prim: &core::SpecializedPrimitive,
+        atom_args: &[core::ResolvedAtomTerm],
+    ) -> Option<(usize, PairProjection, core::ResolvedAtomTerm)> {
+        let col = match prim.name() {
+            "pair-first" => 0usize,
+            "pair-second" => 1usize,
+            _ => return None,
+        };
+        // The atom for `(pair-first p)` is `[p, result]`.
+        if atom_args.len() != 2 {
+            return None;
+        }
+        let proj = self.pair_projections.get(&atom_args[0])?.clone();
+        Some((col, proj, atom_args[1].clone()))
+    }
+
     fn prim(
         &mut self,
         prim: &core::SpecializedPrimitive,
@@ -2548,18 +3183,92 @@ impl<'a> BackendRule<'a> {
     }
 
     fn query(&mut self, query: &core::Query<ResolvedCall, ResolvedVar>, include_subsumed: bool) {
+        // Pre-scan: record the value-column projection for every pair-valued
+        // function result, allocating its two column vars up front. This makes
+        // the `pair-first`/`pair-second` fusion below independent of atom order
+        // (a projection is always known before a primitive that consumes it).
+        for atom in &query.atoms {
+            if let ResolvedCall::Func(f) = &atom.head
+                && let Some((first, second, pair_sort)) = self.pair_info(f)
+            {
+                let result_term = atom
+                    .args
+                    .last()
+                    .expect("function atom must have a result term");
+                let v0: QueryEntry = self.rb.new_var(first.column_ty(self.rb.egraph())).into();
+                let v1: QueryEntry = self.rb.new_var(second.column_ty(self.rb.egraph())).into();
+                self.pair_projections.insert(
+                    result_term.clone(),
+                    PairProjection {
+                        col0: v0,
+                        col1: v1,
+                        first,
+                        second,
+                        pair_sort,
+                    },
+                );
+            }
+        }
         for atom in &query.atoms {
             match &atom.head {
                 ResolvedCall::Func(f) => {
-                    let f = self.func(f);
-                    let args = self.args(&atom.args);
                     let is_subsumed = match include_subsumed {
                         true => None,
                         false => Some(false),
                     };
-                    self.rb.query_table(f, &args, is_subsumed).unwrap();
+                    if let Some(proj) = self.pair_info(f).and(
+                        self.pair_projections
+                            .get(atom.args.last().unwrap())
+                            .cloned(),
+                    ) {
+                        // Pair-valued function: bind the two value columns
+                        // (pre-allocated in the projection) directly.
+                        let backend_f = self.func(f);
+                        let (_result_term, children) = atom
+                            .args
+                            .split_last()
+                            .expect("function atom must have a result term");
+                        let mut args = self.args(children);
+                        args.push(proj.col0.clone());
+                        args.push(proj.col1.clone());
+                        self.rb.query_table(backend_f, &args, is_subsumed).unwrap();
+                    } else {
+                        let backend_f = self.func(f);
+                        let args = self.args(&atom.args);
+                        self.rb.query_table(backend_f, &args, is_subsumed).unwrap();
+                    }
                 }
                 ResolvedCall::Primitive(p) => {
+                    // Fuse `pair-first`/`pair-second` of a pair-valued function
+                    // result directly to its bound value column, avoiding a
+                    // box/unbox roundtrip (keeps the output an indexed column
+                    // for fast rebuild canonicalization).
+                    if let Some((col, src, result)) = self.pair_projection_fusion(p, &atom.args) {
+                        let col_entry = match col {
+                            0 => src.col0,
+                            _ => src.col1,
+                        };
+                        // Alias the projection result directly to the value column
+                        // entry so every use of `result` reads the indexed column.
+                        // But a literal or already-bound result can't be aliased
+                        // (that would drop its equality constraint) — constrain the
+                        // column equal to it instead.
+                        match &result {
+                            core::GenericAtomTerm::Literal(..) => {
+                                let lit_entry = self.entry(&result);
+                                self.rb.assert_eq_entries(lit_entry, col_entry);
+                            }
+                            _ => {
+                                if let Some(existing) = self.entries.get(&result).cloned() {
+                                    // Already bound elsewhere: constrain equal.
+                                    self.rb.assert_eq_entries(existing, col_entry);
+                                } else {
+                                    self.entries.insert(result, col_entry);
+                                }
+                            }
+                        }
+                        continue;
+                    }
                     let ctx = self.query_context();
                     let (p, args, ty) = self.prim(p, &atom.args, ctx);
                     self.rb.query_prim(p, &args, ty).unwrap()
@@ -2573,27 +3282,67 @@ impl<'a> BackendRule<'a> {
             match action {
                 core::GenericCoreAction::Let(span, v, f, args) => {
                     let v = core::GenericAtomTerm::Var(span.clone(), v.clone());
-                    let y = match f {
+                    let y: QueryEntry = match f {
+                        ResolvedCall::Func(f) if self.pair_info(f).is_some() => {
+                            // Pair-valued function lookup: read both value
+                            // columns, then box them into a pair value.
+                            let (first, second, pair_sort) = self.pair_info(f).unwrap();
+                            let name = f.name.clone();
+                            let backend_f = self.func(f);
+                            let args = self.args(args);
+                            let sp0 = span.clone();
+                            let v0: QueryEntry = self
+                                .rb
+                                .lookup_value_col(backend_f, &args, 0, move || {
+                                    format!("{sp0}: lookup of function {name} failed")
+                                })
+                                .into();
+                            let name = f.name.clone();
+                            let sp1 = span.clone();
+                            let v1: QueryEntry = self
+                                .rb
+                                .lookup_value_col(backend_f, &args, 1, move || {
+                                    format!("{sp1}: lookup of function {name} failed")
+                                })
+                                .into();
+                            let ctx = self.action_context();
+                            let ext = self.pair_prim_extid(
+                                "pair",
+                                &[first.clone(), second.clone()],
+                                &pair_sort,
+                                ctx,
+                            );
+                            let ty = pair_sort.column_ty(self.rb.egraph());
+                            self.rb
+                                .call_external_func(ext, &[v0, v1], ty, || {
+                                    "pair construction failed".to_string()
+                                })
+                                .into()
+                        }
                         ResolvedCall::Func(f) => {
                             let name = f.name.clone();
                             let f = self.func(f);
                             let args = self.args(args);
                             let span = span.clone();
-                            self.rb.lookup(f, &args, move || {
-                                format!("{span}: lookup of function {name} failed")
-                            })
+                            self.rb
+                                .lookup(f, &args, move || {
+                                    format!("{span}: lookup of function {name} failed")
+                                })
+                                .into()
                         }
                         ResolvedCall::Primitive(p) => {
                             let name = p.name().to_owned();
                             let ctx = self.action_context();
                             let (p, args, ty) = self.prim(p, args, ctx);
                             let span = span.clone();
-                            self.rb.call_external_func(p, &args, ty, move || {
-                                format!("{span}: call of primitive {name} failed")
-                            })
+                            self.rb
+                                .call_external_func(p, &args, ty, move || {
+                                    format!("{span}: call of primitive {name} failed")
+                                })
+                                .into()
                         }
                     };
-                    self.entries.insert(v, y.into());
+                    self.entries.insert(v, y);
                 }
                 core::GenericCoreAction::LetAtomTerm(span, v, x) => {
                     let v = core::GenericAtomTerm::Var(span.clone(), v.clone());
@@ -2603,9 +3352,21 @@ impl<'a> BackendRule<'a> {
                 core::GenericCoreAction::Set(_, f, xs, y) => match f {
                     ResolvedCall::Primitive(..) => panic!("runtime primitive set!"),
                     ResolvedCall::Func(f) => {
-                        let f = self.func(f);
-                        let args = self.args(xs.iter().chain([y]));
-                        self.rb.set(f, &args)
+                        if let Some((first, second, pair_sort)) = self.pair_info(f) {
+                            // Pair-valued function: unbox the single value `y`
+                            // into the two component value columns.
+                            let backend_f = self.func(f);
+                            let mut args = self.args(xs.iter());
+                            let yv = self.entry(y);
+                            let (v0, v1) = self.unbox_pair_action(yv, &first, &second, &pair_sort);
+                            args.push(v0);
+                            args.push(v1);
+                            self.rb.set(backend_f, &args)
+                        } else {
+                            let backend_f = self.func(f);
+                            let args = self.args(xs.iter().chain([y]));
+                            self.rb.set(backend_f, &args)
+                        }
                     }
                 },
                 core::GenericCoreAction::Change(span, change, f, args) => match f {
@@ -2917,6 +3678,21 @@ mod tests {
         }
     }
 
+    /// A primitive that reads the database can't be used in a `:merge` (a merge is a
+    /// pure write): it has no `Write`-context entrypoint, so it resolves as unbound.
+    #[test]
+    fn read_primitive_in_merge_is_rejected() {
+        let mut egraph = EGraph::default();
+        egraph.add_full_primitive(FullOnly, None);
+        let err = egraph
+            .resolve_program(None, "(function f () i64 :merge (full-only))")
+            .unwrap_err();
+        assert!(
+            matches!(&err, Error::TypeError(TypeError::UnboundFunction(name, _)) if name == "full-only"),
+            "a DB-reading primitive in :merge must be rejected, got {err:?}"
+        );
+    }
+
     #[test]
     fn test_typecheck_expr_with_bindings_and_output_rejects_duplicate_bindings() {
         let mut egraph = EGraph::default();
@@ -3111,6 +3887,33 @@ mod tests {
         assert_eq!(res[0].to_string(), "(expensive)\n");
     }
 
+    #[test]
+    fn test_user_merge_not_identity_short_circuited() {
+        // A user function whose `:merge` body changes the value even when the new
+        // value equals the old one. Ordinary user functions get no `:identity-values`
+        // annotation (only proof-encoding FD views do), so their merge body always
+        // runs: re-setting the same value here must still increment.
+        let mut egraph = EGraph::default();
+        egraph
+            .parse_and_run_program(
+                None,
+                r#"
+                (function counter () i64 :merge (+ old 1))
+                (set (counter) 5)
+                (set (counter) 5)
+                (check (= (counter) 6))
+                "#,
+            )
+            .unwrap();
+
+        // Sanity: the same key inserted with an equal value collides and the
+        // merge runs (classic behavior). Were it short-circuited (as a universal
+        // `Some(1)` would do), `(counter)` would stay 5 and this check would fail.
+        egraph
+            .parse_and_run_program(None, "(check (!= (counter) 5))")
+            .unwrap();
+    }
+
     #[test]
     fn test_run_undefined_ruleset_errors() {
         let mut egraph = EGraph::default();
diff --git a/src/prelude.rs b/src/prelude.rs
index f2b2e7d38..608e171b2 100644
--- a/src/prelude.rs
+++ b/src/prelude.rs
@@ -733,9 +733,11 @@ pub fn add_function(
         name: name.to_owned(),
         schema,
         merge,
+        merge_action: Default::default(),
         hidden: false,
         let_binding: false,
         term_constructor: None,
+        identity_values: None,
         unextractable: false,
     }])
 }
@@ -881,7 +883,7 @@ pub trait ContainerSort: Any + Send + Sync + Debug {
 }
 
 #[derive(Debug)]
-struct ContainerSortImpl<T: ContainerSort>(T);
+pub(crate) struct ContainerSortImpl<T: ContainerSort>(pub(crate) T);
 
 impl<T: ContainerSort> Sort for ContainerSortImpl<T> {
     fn name(&self) -> &str {
diff --git a/src/proofs/proof_checker.rs b/src/proofs/proof_checker.rs
index a24dcd0bc..0dba417fc 100644
--- a/src/proofs/proof_checker.rs
+++ b/src/proofs/proof_checker.rs
@@ -73,6 +73,73 @@ pub(crate) fn run_merge(
     .into())
 }
 
+/// Find the subexpression at pre-order position `idx` in `expr`'s tree (index 0 is
+/// `expr` itself). Must mirror the indexing the proof encoder uses to tag
+/// `MergeFnIdx` proofs.
+fn subexpr_at_index(expr: &ResolvedExpr, idx: usize) -> Option<&ResolvedExpr> {
+    let mut counter = 0;
+    fn walk<'a>(
+        expr: &'a ResolvedExpr,
+        target: usize,
+        counter: &mut usize,
+    ) -> Option<&'a ResolvedExpr> {
+        if *counter == target {
+            return Some(expr);
+        }
+        *counter += 1;
+        if let ResolvedExpr::Call(_, _, args) = expr {
+            for arg in args {
+                if let Some(found) = walk(arg, target, counter) {
+                    return Some(found);
+                }
+            }
+        }
+        None
+    }
+    walk(expr, idx, &mut counter)
+}
+
+/// Run subexpression `idx` of a function's merge body and return the resulting
+/// term plus propositions learned. `idx` is a pre-order index over the merge body
+/// expression tree (see [`subexpr_at_index`]); `idx == 0` is the whole body.
+///
+/// `old`/`new` are bound to `old_term`/`new_term`. Evaluating the subexpression
+/// reconstructs the term that the FD custom-function view merge minted at that
+/// position, so each nested merge-body subexpression yields its own conclusion.
+pub(crate) fn run_merge_subexpr(
+    term_dag: &mut TermDag,
+    func_name: &str,
+    prog: &[ResolvedNCommand],
+    old_term: TermId,
+    new_term: TermId,
+    idx: usize,
+) -> Result<(TermId, HashSet<Proposition>), ProofCheckError> {
+    let mut subst = HashMap::default();
+    subst.insert("old".to_string(), old_term);
+    subst.insert("new".to_string(), new_term);
+    for cmd in prog {
+        if let GenericNCommand::Function(func_decl) = cmd
+            && func_decl.name == func_name
+        {
+            let expr = func_decl.merge.as_ref().ok_or_else(|| {
+                ProofCheckError::from(ProofCheckErrorKind::FunctionNotFound {
+                    function_name: func_name.to_string(),
+                })
+            })?;
+            let subexpr = subexpr_at_index(expr, idx).ok_or_else(|| {
+                ProofCheckError::from(ProofCheckErrorKind::FunctionNotFound {
+                    function_name: format!("{func_name} (merge subexpr index {idx} out of range)"),
+                })
+            })?;
+            return eval_expr_with_subst("merge_function", subexpr, term_dag, &subst);
+        }
+    }
+    Err(ProofCheckErrorKind::FunctionNotFound {
+        function_name: func_name.to_string(),
+    }
+    .into())
+}
+
 /// Given a sequence of actions, computes:
 /// 1. All the terms bound to variables (from Let actions)
 /// 2. All the propositions implied by the actions:
diff --git a/src/proofs/proof_encoding.md b/src/proofs/proof_encoding.md
index c0866b85a..ad34b7106 100644
--- a/src/proofs/proof_encoding.md
+++ b/src/proofs/proof_encoding.md
@@ -40,22 +40,22 @@ Lowering the program with the term encoding expands to a bunch of new egglog, wh
 
 ```text
 (ruleset parent)
-(ruleset single_parent)
 (ruleset uf_function_index)
 (ruleset rebuilding)
 (ruleset rebuilding_cleanup)
 (ruleset delete_subsume_ruleset)
 ```
 
-*The new rulesets* orchestrate new rules for per-sort union-find tables (`parent` and `single_parent`),
+*The new rulesets* orchestrate new rules for the per-sort union-find table (`parent`),
 building a fast function index over UF (`uf_function_index`),
 rebuild-time congruence (`rebuilding` + `rebuilding_cleanup`), and deferred deletions/subsumptions (`delete_subsume_ruleset`).
+The single-parent invariant (each term points to a single parent) is no longer a
+separate ruleset: it is maintained by the UF function index's own `:merge` (see below).
 
 ```text
 (run-schedule
     (saturate
        rebuilding_cleanup ;; cleanup merged rows
-       (saturate single_parent) ;; ensure each term points to single parent
        (saturate parent) ;; transitively close parent links
        (saturate uf_function_index) ;; mirror UF constructor rows into UF function index
        rebuilding) ;; find new equalities via congruence
@@ -68,7 +68,9 @@ rebuild-time congruence (`rebuilding` + `rebuilding_cleanup`), and deferred dele
 ```text
 (sort Math)
 (function UF_Math (Math Math) Unit :merge old :internal-hidden)
-(function UF_Mathf (Math) Math :merge new)
+(function UF_Mathf (Math) Math
+  :merge ((set (UF_Math (ordering-max old new) (ordering-min old new)) ())
+          (ordering-min old new)))
 ```
 
 *The union-find* tables for each sort store the equivalence
@@ -88,27 +90,33 @@ When proof tracking is enabled, proofs are stored directly in the UF table
      ((delete (UF_Math a b))
       (set (UF_Math a c) ()))
        :ruleset parent :name "uf_update")
-(rule ((UF_Math a b)
-      (UF_Math a c)
-      (!= b c)
-      (= (ordering-max b c) b))
-     ((delete (UF_Math a b))
-      (set (UF_Math b c) ()))
-       :ruleset single_parent :name "singleparentuf_update")
 (rule ((UF_Math a b))
       ((set (UF_Mathf a) b))
        :ruleset uf_function_index :name "uf_function_index_update")
 ```
 
 *Union-find rules:*
-A couple rules ensure the UF function is kept up to date as
-  equalities are added, and the indexing ruleset mirrors those rows
-  into the function UF.
+The `parent` ruleset performs path compression (chasing `a -> b -> c` to point `a`
+  straight at the representative), and the `uf_function_index` ruleset mirrors UF
+  rows into the function index `UF_<Sort>f`.
 We use the `ordering-max` and `ordering-min` egglog primitives
   to define an arbitrary ordering on terms based on insertion order,
   so that we can deterministically choose which term becomes the parent
   in the union-find structure.
 
+*The single-parent invariant* (each source term has at most one parent) is
+  maintained by the `UF_<Sort>f` index's `:merge` rather than a separate rule.
+The index rule is the only writer of `(UF_<Sort>f a)`, so a key collision means
+  source `a` has two parents `b` and `c`. The merge then unions those two parents
+  by writing the edge `(UF_<Sort> (ordering-max b c) (ordering-min b c))` back into
+  the UF table and keeping `(ordering-min b c)` as `a`'s surviving leader. Path
+  compression subsequently chases `a -> max -> min` and deletes the now-redundant
+  `(UF_<Sort> a max)` row, so the UF table converges to one parent per source.
+With proof tracking, the index value is a `(Pair leader proof)` (the proof proves
+  `a = leader`); the merge composes the union proof via `Trans`/`Sym`, orienting it
+  with `select-eq` so the surviving row keeps an existing premise proof verbatim
+  (which keeps the value stable so the merge saturates).
+
 **Important invariant:** every representative term must have a self-loop
   entry in the constructor union-find table (e.g., `(UF_Math v v)`).
 This is because the rebuild rules query the union-find for every
diff --git a/src/proofs/proof_encoding.rs b/src/proofs/proof_encoding.rs
index d0c3fc3f0..41b358183 100644
--- a/src/proofs/proof_encoding.rs
+++ b/src/proofs/proof_encoding.rs
@@ -8,6 +8,13 @@ use crate::*;
 pub(crate) struct EncodingState {
     pub uf_parent: HashMap<String, String>,
     pub uf_function: HashMap<String, String>,
+    /// Per-sort name of the `(Pair sort proof)` sort, shared by the UF function
+    /// index and the FD view value column. Memoized so all references agree.
+    pub uf_pair_sort: HashMap<String, String>,
+    /// Names of functions declared with the FD pair-valued view (constructors and
+    /// primitive-bodied custom functions). Used so action/rebuild sites route the
+    /// same way the view declaration did.
+    pub fd_view_funcs: HashSet<String>,
     /// Maps sort name -> proof function name (set from :internal-proof-func annotation).
     pub proof_func_parent: HashMap<String, String>,
     pub term_header_added: bool,
@@ -29,6 +36,8 @@ impl EncodingState {
         Self {
             uf_parent: HashMap::default(),
             uf_function: HashMap::default(),
+            uf_pair_sort: HashMap::default(),
+            fd_view_funcs: HashSet::default(),
             proof_func_parent: HashMap::default(),
             term_header_added: false,
             original_typechecking: None,
@@ -54,6 +63,151 @@ impl<'a> ProofInstrumentor<'a> {
         Self { egraph }.add_term_encoding_helper(program)
     }
 
+    /// Whether `fdecl` uses the FD pair-valued view (`(children) -> (pair output proof)`,
+    /// keyed on children only). Constructors always do; a custom function does iff its
+    /// `:merge` body is:
+    ///   - primitive-bodied (every call a primitive, e.g. `min`/`max`), for any
+    ///     non-eq-sort output, or a trivial value-replacement (bare `old`/`new` or a
+    ///     literal) for an eq-sort output; or
+    ///   - constructor-bodied (calls only user constructors, minted via `fd-mint`).
+    ///
+    /// Live-DB-reading and non-global `:no-merge` customs are rejected earlier by
+    /// `command_supports_proof_encoding`, so they never reach the encoder.
+    pub(crate) fn is_fd_pair_view(&self, fdecl: &ResolvedFunctionDecl) -> bool {
+        match fdecl.subtype {
+            FunctionSubtype::Constructor => true,
+            FunctionSubtype::Custom => {
+                self.is_primitive_bodied_fd_custom(fdecl)
+                    || self.is_constructor_bodied_fd_custom(fdecl)
+            }
+        }
+    }
+
+    /// True iff `fdecl` is a custom function whose `:merge` body mints constructors
+    /// (and may call primitives), making it eligible for the FD pair-valued view
+    /// (Phase B). Calls to non-constructor user functions are not supported here.
+    /// Inputs and output may both be eq-sorts: eq-sort inputs verify via Phase C's
+    /// `reflexivize_premise` (proof_format.rs).
+    ///
+    /// Such a merge mints constructor enodes, but in a fixpoint analysis most
+    /// collisions are no-ops (merged output equals the existing one). The backend
+    /// identity-column short-circuit (`FunctionConfig::identity_values = Some(1)`)
+    /// keeps the existing row on an unchanged output and skips the minting body, so
+    /// we don't mint spurious nodes and diverge from normal mode.
+    fn is_constructor_bodied_fd_custom(&self, fdecl: &ResolvedFunctionDecl) -> bool {
+        if fdecl.subtype != FunctionSubtype::Custom {
+            return false;
+        }
+        match &fdecl.merge {
+            None => false,
+            Some(merge) => {
+                // Must call a user constructor (else it is primitive-bodied), and
+                // every user-function call must be a constructor (so it can be minted).
+                Self::merge_body_calls_constructor(merge)
+                    && Self::merge_body_funcs_all_constructors(merge)
+            }
+        }
+    }
+
+    /// Whether the merge body contains at least one user-function call.
+    fn merge_body_calls_constructor(expr: &ResolvedExpr) -> bool {
+        match expr {
+            ResolvedExpr::Lit(..) | ResolvedExpr::Var(..) => false,
+            ResolvedExpr::Call(_, ResolvedCall::Func(_), _) => true,
+            ResolvedExpr::Call(_, ResolvedCall::Primitive(_), args) => {
+                args.iter().any(Self::merge_body_calls_constructor)
+            }
+        }
+    }
+
+    /// Whether every user-function call in the merge body targets a CONSTRUCTOR.
+    fn merge_body_funcs_all_constructors(expr: &ResolvedExpr) -> bool {
+        match expr {
+            ResolvedExpr::Lit(..) | ResolvedExpr::Var(..) => true,
+            ResolvedExpr::Call(_, ResolvedCall::Func(f), args) => {
+                f.subtype == FunctionSubtype::Constructor
+                    && args.iter().all(Self::merge_body_funcs_all_constructors)
+            }
+            ResolvedExpr::Call(_, ResolvedCall::Primitive(_), args) => {
+                args.iter().all(Self::merge_body_funcs_all_constructors)
+            }
+        }
+    }
+
+    /// True iff `fdecl` is a custom function with a primitive-bodied `:merge` that is
+    /// eligible for the FD pair-valued view.
+    fn is_primitive_bodied_fd_custom(&self, fdecl: &ResolvedFunctionDecl) -> bool {
+        if fdecl.subtype != FunctionSubtype::Custom {
+            return false;
+        }
+        // Eq-sort inputs are allowed (Phase C): rebuild re-keys the view row and
+        // rewrites its proof into a congruence proof. The FD merge's `MergeRow`/
+        // `MergeIdx` justification needs reflexive premises, so at resugaring time
+        // each congruence premise is reflexivized. See `reflexivize_premise` in
+        // proof_format.rs.
+        let merge = match &fdecl.merge {
+            None => return false,
+            Some(merge) => merge,
+        };
+        // For a non-eq-sort output any primitive-bodied merge works (the output is a
+        // plain value/lattice sort, no union-find). For an eq-sort output we allow
+        // only a trivial value-replacement body (bare `old`/`new`), which keeps one
+        // colliding output without computing a new term; a primitive call could
+        // synthesize a fresh eq-sort value needing a union, which this path can't do.
+        let output_is_eq_sort = self
+            .egraph
+            .type_info
+            .get_sort_by_name(&fdecl.schema.output)
+            .map(|s| s.is_eq_sort())
+            .unwrap_or(true);
+        if output_is_eq_sort {
+            return Self::merge_body_is_trivial(merge);
+        }
+        Self::merge_body_is_all_primitive(merge)
+    }
+
+    /// Whether a (resolved) merge body is a trivial value-replacement: a bare variable
+    /// (`old`/`new`) or a literal. Such a merge keeps one of the two colliding outputs
+    /// verbatim without computing a new value, so it is safe even for an eq-sort output
+    /// (no new eq-sort term is minted and no union is needed).
+    fn merge_body_is_trivial(expr: &ResolvedExpr) -> bool {
+        matches!(expr, ResolvedExpr::Lit(..) | ResolvedExpr::Var(..))
+    }
+
+    /// Whether every call in a (resolved) merge body is a primitive call (no calls
+    /// to user functions/constructors). Vars and literals are fine.
+    fn merge_body_is_all_primitive(expr: &ResolvedExpr) -> bool {
+        match expr {
+            ResolvedExpr::Lit(..) | ResolvedExpr::Var(..) => true,
+            ResolvedExpr::Call(_, ResolvedCall::Func(_), _) => false,
+            ResolvedExpr::Call(_, ResolvedCall::Primitive(_), args) => {
+                args.iter().all(Self::merge_body_is_all_primitive)
+            }
+        }
+    }
+
+    /// Whether the function with the given name was declared with the FD pair-valued
+    /// view. Populated by [`Self::term_and_view`] when it declares the view table, so
+    /// later action/rebuild sites (which only have the function name / [`FuncType`])
+    /// can route consistently. Constructors are always FD even before being recorded.
+    pub(crate) fn name_is_fd_pair_view(&self, name: &str) -> bool {
+        // Rely solely on the recorded set: `term_and_view` records every FD function
+        // when it declares the view. Don't fall back to `get_func_type(name)` — by
+        // now the encoder has redeclared the original name as the hidden inner term
+        // constructor, so `get_func_type` would misreport a legacy custom as a
+        // constructor.
+        self.egraph.proof_state.fd_view_funcs.contains(name)
+    }
+
+    /// Like [`Self::name_is_fd_pair_view`], for a resolved [`FuncType`] at an action
+    /// site (the view declaration has already recorded FD custom functions by name).
+    pub(crate) fn func_type_is_fd_pair_view(&self, func_type: &FuncType) -> bool {
+        if func_type.subtype == FunctionSubtype::Constructor {
+            return true;
+        }
+        self.name_is_fd_pair_view(&func_type.name)
+    }
+
     /// Mark two things as equal, adding proof if proofs are enabled.
     pub(crate) fn union(
         &mut self,
@@ -80,9 +234,6 @@ impl<'a> ProofInstrumentor<'a> {
                 Justification::Fiat => format!(
                     "({fiat_constructor} ({to_ast_constructor} {larger}) ({to_ast_constructor} {smaller}))"
                 ),
-                Justification::Merge(_func_name, _proof1, _proof2) => panic!(
-                    "Merge functions do not include union actions, so proof should not be by merge"
-                ),
                 Justification::Proof(existing_proof) => existing_proof.clone(),
             }
         } else {
@@ -102,7 +253,6 @@ impl<'a> ProofInstrumentor<'a> {
         let uf_function_index_name = self.egraph.parser.symbol_gen.fresh("uf_function_index");
 
         let path_compress_ruleset_name = self.proof_names().path_compress_ruleset_name.clone();
-        let single_parent_ruleset_name = self.proof_names().single_parent_ruleset_name.clone();
         let uf_function_index_ruleset_name =
             self.proof_names().uf_function_index_ruleset_name.clone();
 
@@ -110,81 +260,103 @@ impl<'a> ProofInstrumentor<'a> {
 
         // In proof mode, path compression composes proofs via Trans/Sym.
         // In term mode, the proof output is Unit and we just write ().
-        let (path_compress_query, path_compress_action, single_parent_query, single_parent_action) =
-            if self.egraph.proof_state.proofs_enabled {
-                let p1_fresh = self.egraph.parser.symbol_gen.fresh("p1");
-                let p2_fresh = self.egraph.parser.symbol_gen.fresh("p2");
-                let trans = self.proof_names().eq_trans_constructor.clone();
-                let sym = self.proof_names().eq_sym_constructor.clone();
-                (
-                    format!(
-                        "(= {p1_fresh} ({pname} a b))
+        let (path_compress_query, path_compress_action) = if self.egraph.proof_state.proofs_enabled
+        {
+            let p1_fresh = self.egraph.parser.symbol_gen.fresh("p1");
+            let p2_fresh = self.egraph.parser.symbol_gen.fresh("p2");
+            let trans = self.proof_names().eq_trans_constructor.clone();
+            (
+                format!(
+                    "(= {p1_fresh} ({pname} a b))
                         (= {p2_fresh} ({pname} b c))"
-                    ),
-                    format!(
-                        "(delete ({pname} a b))
+                ),
+                format!(
+                    "(delete ({pname} a b))
                        (set ({pname} a c) ({trans} {p1_fresh} {p2_fresh}))"
-                    ),
-                    format!(
-                        "(= {p1_fresh} ({pname} a b))
-                        (= {p2_fresh} ({pname} a c))"
-                    ),
-                    format!(
-                        "(delete ({pname} a b))
-                       (set ({pname} b c) ({trans} ({sym} {p1_fresh}) {p2_fresh}))"
-                    ),
-                )
-            } else {
-                (
-                    format!("({pname} a b)\n                        ({pname} b c)"),
-                    format!(
-                        "(delete ({pname} a b))\n                       (set ({pname} a c) ())"
-                    ),
-                    format!("({pname} a b)\n                        ({pname} a c)"),
-                    format!(
-                        "(delete ({pname} a b))\n                       (set ({pname} b c) ())"
-                    ),
-                )
-            };
+                ),
+            )
+        } else {
+            (
+                format!("({pname} a b)\n                        ({pname} b c)"),
+                format!("(delete ({pname} a b))\n                       (set ({pname} a c) ())"),
+            )
+        };
 
-        // In proof mode, UF function index stores (leader, proof) pairs.
-        // In term mode, it just stores the leader.
-        let (uf_function_output_type, uf_pair_sort_decl, uf_index_query, uf_index_action) =
-            if self.egraph.proof_state.proofs_enabled {
-                let pair_sort = self.uf_pair_sort_name(sort_name);
-                let proof_fresh = self.egraph.parser.symbol_gen.fresh("uf_idx_proof");
-                (
-                    pair_sort.clone(),
-                    format!("(sort {pair_sort} (Pair {sort_name} {proof_type}))"),
-                    format!("(= {proof_fresh} ({pname} a b))"),
-                    format!("(set ({uf_function_name} a) (pair b {proof_fresh}))"),
-                )
-            } else {
-                (
-                    sort_name.to_string(),
-                    "".to_string(),
-                    format!("({pname} a b)"),
-                    format!("(set ({uf_function_name} a) b)"),
-                )
-            };
+        // The UF function index stores, per source term, the current leader (plus a
+        // proof in proof mode). A key collision means one source `a` has two parents,
+        // and its `:merge` resolves it: keep the smaller leader and write the union
+        // edge between the parents back into the constructor UF table. Path
+        // compression then converges the table to a single parent per source — the
+        // work the old `single_parent` rule did, now folded into the merge.
+        let (
+            uf_function_output_type,
+            uf_pair_sort_decl,
+            uf_index_query,
+            uf_index_action,
+            uf_index_merge,
+        ) = if self.egraph.proof_state.proofs_enabled {
+            let pair_sort = self.uf_pair_sort_name(sort_name);
+            let proof_fresh = self.egraph.parser.symbol_gen.fresh("uf_idx_proof");
+            let trans = self.proof_names().eq_trans_constructor.clone();
+            let sym = self.proof_names().eq_sym_constructor.clone();
+            // old = (pair leader_o p_o), p_o proves a = leader_o.
+            // new = (pair leader_n p_n), p_n proves a = leader_n.
+            let lo = "(pair-first old)";
+            let po = "(pair-second old)";
+            let ln = "(pair-first new)";
+            let pn = "(pair-second new)";
+            let larger = format!("(ordering-max {lo} {ln})");
+            let smaller = format!("(ordering-min {lo} {ln})");
+            // Proof that larger = smaller, oriented by which leader is larger.
+            // If leader_o is the larger one: leader_o = leader_n via Trans(Sym p_o, p_n).
+            // Otherwise leader_n is larger: leader_n = leader_o via Trans(Sym p_n, p_o).
+            let union_proof = format!(
+                "(select-eq {larger} {lo} ({trans} ({sym} {po}) {pn}) ({trans} ({sym} {pn}) {po}))"
+            );
+            // The surviving index proof must prove a = smaller; keep the existing
+            // premise proof for whichever leader is the smaller one (value-stable,
+            // so the row saturates instead of minting a fresh proof each iteration).
+            let surviving_proof = format!("(select-eq {smaller} {lo} {po} {pn})");
+            // Block-form merge: write the parent-union edge into the UF table,
+            // then return the surviving (leader, proof) pair.
+            let merge = format!(
+                "((set ({pname} {larger} {smaller}) {union_proof}) (pair {smaller} {surviving_proof}))"
+            );
+            (
+                pair_sort.clone(),
+                format!("(sort {pair_sort} (Pair {sort_name} {proof_type}))"),
+                format!("(= {proof_fresh} ({pname} a b))"),
+                format!("(set ({uf_function_name} a) (pair b {proof_fresh}))"),
+                merge,
+            )
+        } else {
+            // Term mode: index value is just the leader. The merge writes the
+            // parent-union edge and keeps the smaller leader.
+            let merge = format!(
+                "((set ({pname} (ordering-max old new) (ordering-min old new)) ()) (ordering-min old new))"
+            );
+            (
+                sort_name.to_string(),
+                "".to_string(),
+                format!("({pname} a b)"),
+                format!("(set ({uf_function_name} a) b)"),
+                merge,
+            )
+        };
 
         let mut code = format!(
             "{uf_pair_sort_decl}
              (function {pname} ({sort_name} {sort_name}) {proof_type} :merge old :internal-hidden)
-             (function {uf_function_name} ({sort_name}) {uf_function_output_type} :merge new :unextractable :internal-hidden)
+             ;; The index's :merge folds in the single-parent invariant: a key
+             ;; collision (one source with two parents) unions the parents back into
+             ;; the UF table and keeps the smaller leader.
+             (function {uf_function_name} ({sort_name}) {uf_function_output_type} :merge {uf_index_merge} :unextractable :internal-hidden)
              ;; performs path compression, ensuring each term points to the representative
              (rule ({path_compress_query}
                     (!= b c))
                   ({path_compress_action})
                    :ruleset {path_compress_ruleset_name}
                    :name \"{fresh_name}\")
-             ;; ensures each term has only one parent
-             (rule ({single_parent_query}
-                    (!= b c)
-                    (= (ordering-max b c) b))
-                  ({single_parent_action})
-                   :ruleset {single_parent_ruleset_name}
-                   :name \"singleparent{fresh_name}\")
              ;; mirrors UF rows into a function-backed UF index for faster rebuild lookups
              (rule ({uf_index_query})
                    ({uf_index_action})
@@ -222,190 +394,254 @@ impl<'a> ProofInstrumentor<'a> {
         let delete_subsume_ruleset = self.proof_names().delete_subsume_ruleset_name.clone();
         let fresh_name = self.egraph.parser.symbol_gen.fresh("delete_rule");
 
-        format!(
-            "(rule (({to_delete_name} {child_names})
-                    ({view_name} {child_names} out))
-                   ((delete ({view_name} {child_names} out))
-                    (delete ({to_delete_name} {child_names})))
-                    :ruleset {delete_subsume_ruleset}
-                    :name \"{fresh_name}\")
-             (rule (({subsumed_name} {child_names})
-                    ({view_name} {child_names} out))
-                   ((subsume ({view_name} {child_names} out)))
-                    :ruleset {delete_subsume_ruleset}
-                    :name \"{fresh_name}_subsume\")"
-        )
-    }
-
-    /// Generate rules that run a merge function for a custom function.
-    /// One rule runs the merge function when two different values are present for the same children.
-    /// Another rule cleans up old values, necessary because the newly merged value may be equal to one of the old values.
-    fn handle_merge_fn(
-        &mut self,
-        fdecl: &ResolvedFunctionDecl,
-        child_names: &[String],
-        child_names_str: &str,
-        _view_name: &str,
-        rebuilding_ruleset: &str,
-    ) -> String {
-        let name = &fdecl.name;
-
-        let merge_fn = &fdecl
-            .merge
-            .as_ref()
-            .unwrap_or_else(|| panic!("Proofs don't support :no-merge"));
-
-        let fresh_name = self.egraph.parser.symbol_gen.fresh("merge_rule");
-        let cleanup_name = self.egraph.parser.symbol_gen.fresh("merge_cleanup");
-
-        let p1_fresh = self.egraph.parser.symbol_gen.fresh("p1");
-        let p2_fresh = self.egraph.parser.symbol_gen.fresh("p2");
-        let view_name = self.view_name(&fdecl.name);
-        let rebuilding_cleanup_ruleset = self.proof_names().rebuilding_cleanup_ruleset_name.clone();
-        let proof_query = if self.egraph.proof_state.proofs_enabled {
-            // View is a function with proof output; bind proof variables
+        if self.is_fd_pair_view(fdecl) {
+            // FD view: the key is the children only (the output is the value),
+            // so we delete/subsume by the children key. Bind the value with
+            // `out` only to guard that the row exists.
             format!(
-                "(= {p1_fresh} ({view_name} {child_names_str} old))
-                     (= {p2_fresh} ({view_name} {child_names_str} new))
-                    "
+                "(rule (({to_delete_name} {child_names})
+                        (= out ({view_name} {child_names})))
+                       ((delete ({view_name} {child_names}))
+                        (delete ({to_delete_name} {child_names})))
+                        :ruleset {delete_subsume_ruleset}
+                        :name \"{fresh_name}\")
+                 (rule (({subsumed_name} {child_names})
+                        (= out ({view_name} {child_names})))
+                       ((subsume ({view_name} {child_names})))
+                        :ruleset {delete_subsume_ruleset}
+                        :name \"{fresh_name}_subsume\")"
             )
         } else {
-            // View is a function with Unit output; no need to bind the output
-            "".to_string()
-        };
-        let proof_var = if self.egraph.proof_state.proofs_enabled {
-            self.fresh_var()
+            format!(
+                "(rule (({to_delete_name} {child_names})
+                        ({view_name} {child_names} out))
+                       ((delete ({view_name} {child_names} out))
+                        (delete ({to_delete_name} {child_names})))
+                        :ruleset {delete_subsume_ruleset}
+                        :name \"{fresh_name}\")
+                 (rule (({subsumed_name} {child_names})
+                        ({view_name} {child_names} out))
+                       ((subsume ({view_name} {child_names} out)))
+                        :ruleset {delete_subsume_ruleset}
+                        :name \"{fresh_name}_subsume\")"
+            )
+        }
+    }
+
+    /// Generate the rules (if any) that handle a function's merge or congruence.
+    ///
+    /// All proof-supported merges are handled in the FD view's own `:merge`, so this
+    /// emits no extra rule. Live-DB-reading merges (`LookupInMergeDisallowed`) and
+    /// non-global `:no-merge` customs (`NoMergeOnNonGlobalFunction`, #774) are
+    /// rejected at typecheck, before encoding, so neither reaches here.
+    fn handle_merge_or_congruence(&mut self, fdecl: &ResolvedFunctionDecl) -> String {
+        if fdecl.subtype == FunctionSubtype::Custom && !self.is_fd_pair_view(fdecl) {
+            unreachable!(
+                "custom merge in a proof-supported program must be FD; function-reading merges are rejected by the LookupInMergeDisallowed typecheck error"
+            )
+        }
+        String::new()
+    }
+
+    /// The `:merge` expression for a constructor's FD view table.
+    ///
+    /// The FD view maps `(children) -> output`, so when two terms with the
+    /// same children have different outputs (i.e. they are congruent) the
+    /// key collides and this merge runs. It unions the two outputs by writing
+    /// the union-find parent edge on the side with a block-merge `set`, then
+    /// keeps the smaller representative as the surviving output.
+    fn constructor_view_merge(&mut self, out_type: &str) -> String {
+        let uf = self.uf_name(out_type);
+        // Block-form merge: as an effect, record the congruence union edge in
+        // the UF table on the side (a `set` action — it names `uf` statically
+        // so the backend declares the write-dependency); then the value is the
+        // smaller representative.
+        if self.egraph.proof_state.proofs_enabled {
+            // The view value is a `(pair output proof)` (two value columns);
+            // `old`/`new` are the two colliding pairs (both reps of the same
+            // f(children), since they collided on the view key). The proof in
+            // each pair proves `output = f(children)`. We orient them by the
+            // ordering of the outputs and build the congruence union proof
+            // `Trans(p_large, Sym(p_small))` proving `larger = smaller`.
+            let trans = self.proof_names().eq_trans_constructor.clone();
+            let sym = self.proof_names().eq_sym_constructor.clone();
+            let oo = "(pair-first old)";
+            let on = "(pair-first new)";
+            let po = "(pair-second old)";
+            let pn = "(pair-second new)";
+            let larger = format!("(ordering-max {oo} {on})");
+            let smaller = format!("(ordering-min {oo} {on})");
+            // p_large proves `larger = f(children)`, p_small proves
+            // `smaller = f(children)`. select-eq picks the proof of whichever
+            // output equals larger/smaller. On a tie (oo == on) both pick the
+            // OLD proof `po`, so the surviving value is unchanged and the merge
+            // does not re-fire forever.
+            let p_large = format!("(select-eq {larger} {oo} {po} {pn})");
+            let p_small = format!("(select-eq {smaller} {oo} {po} {pn})");
+            let union_proof = format!("({trans} {p_large} ({sym} {p_small}))");
+            format!("((set ({uf} {larger} {smaller}) {union_proof}) (pair {smaller} {p_small}))")
         } else {
-            "()".to_string()
-        };
-        let mut merge_fn_code = vec![];
-        let merge_fn_var = self.instrument_action_expr(
-            merge_fn,
-            &mut merge_fn_code,
-            &Justification::Merge(name.clone(), p1_fresh.clone(), p2_fresh.clone()),
-        );
-        let merge_fn_code_str = merge_fn_code.join("\n");
-        let mut updated = child_names.to_vec();
-        updated.push(merge_fn_var.clone());
-        let term = format!("({name} {child_names_str} {merge_fn_var})");
-
-        let rule_proof = if self.egraph.proof_state.proofs_enabled {
-            let to_ast = self.fname_to_ast_name(name);
-            let merge_fn_constructor = self.proof_names().merge_fn_constructor.clone();
+            // Term-encoding mode (no proofs): the view value is the output (an
+            // eclass id) directly, and the UF proof column is Unit.
             format!(
-                "(let {proof_var}
-                            ({merge_fn_constructor} \"{name}\"
-                                  {p1_fresh}
-                                  {p2_fresh}
-                                  ({to_ast} {term})))"
+                "((set ({uf} (ordering-max old new) (ordering-min old new)) ()) (ordering-min old new))"
             )
+        }
+    }
+
+    /// The `:merge` expression for a primitive-bodied custom function's FD view
+    /// (`(children) -> (pair output proof)`). On a children-key collision the merge
+    /// runs the user's primitive body on the two output columns and produces a
+    /// `MergeIdx` justification — unlike a constructor, there is no union. In term
+    /// mode the view value is the output directly and the merge is just that body.
+    fn custom_fd_view_merge(&mut self, fname: &str, merge: &ResolvedExpr) -> String {
+        if self.egraph.proof_state.proofs_enabled {
+            // `old`/`new` in the user merge body refer to the output value, which in
+            // the pair-view lives in `(pair-first old)`/`(pair-first new)`.
+            let body = Self::render_merge_on_pair_first(merge);
+            let merge_row = self.proof_names().merge_fn_row_constructor.clone();
+            // The proof column. `MergeRow` reconstructs the top view row by evaluating
+            // the merge body on the premise outputs. For stability, when the merged
+            // output equals a premise output (common for `min`/`max`/lattice ops) the
+            // `select-eq` keeps that premise's existing proof, so the surviving row is
+            // identical and the merge saturates; otherwise it mints a fresh `MergeRow`.
+            let fresh = format!("({merge_row} \"{fname}\" (pair-second old) (pair-second new))");
+            let proof = format!(
+                "(select-eq {body} (pair-first old) (pair-second old) \
+                  (select-eq {body} (pair-first new) (pair-second new) {fresh}))"
+            );
+            format!("(pair {body} {proof})")
         } else {
-            "".to_string()
-        };
-        let term_and_proof = self.update_view(name, &updated, &proof_var);
-        let cleanup_constructor = self.egraph.parser.symbol_gen.fresh("mergecleanup");
-        let fresh_sort = self.egraph.parser.symbol_gen.fresh("mergecleanupsort");
-        let output_sort = fdecl.schema.output.clone();
-
-        // The first runs the merge function adding a new row.
-        // The second deletes rows with old values for the old variable, while the third deletes rows with new values for the new variable.
-        format!(
-            "(sort {fresh_sort})
-                 (constructor {cleanup_constructor} ({output_sort} {output_sort}) {fresh_sort} :internal-hidden)
-                 (rule (({view_name} {child_names_str} old)
-                        ({view_name} {child_names_str} new)
-                        (!= old new)
-                        (= (ordering-max old new) new)
-                        {proof_query})
-                       (
-                        {merge_fn_code_str}
-                        {rule_proof}
-                        {term_and_proof}
-                        ({cleanup_constructor} {merge_fn_var} old)
-                        ({cleanup_constructor} {merge_fn_var} new)
-                       )
-                        :ruleset {rebuilding_ruleset}
-                        :name \"{fresh_name}\")
-                 (rule (({cleanup_constructor} merged old)
-                        ({view_name} {child_names_str} merged)
-                        ({view_name} {child_names_str} old)
-                        (!= merged old))
-                       ((delete ({view_name} {child_names_str} old)))
-                        :ruleset {rebuilding_cleanup_ruleset}
-                        :name \"{cleanup_name}\")
-                ",
-        )
+            Self::render_merge_on_old_new(merge)
+        }
     }
 
-    /// Generate a rule that handles congruence for constructors.
-    /// When two different values are present for the same children,
-    /// we union those two values together.
-    fn handle_congruence(
+    /// The `:merge` expression for a constructor-bodied custom function's FD view
+    /// (Phase B). Like [`Self::custom_fd_view_merge`], but each constructor node
+    /// `(C a b)` is rendered as a `fd-mint` carrying a `MergeIdx(f, p_old, p_new, idx)`
+    /// existence proof (idx = pre-order position over body nodes). The output column
+    /// is the nested tree of `fd-mint`s; the f-view proof column is `MergeRow(...)`.
+    fn constructor_bodied_fd_view_merge(&mut self, fname: &str, merge: &ResolvedExpr) -> String {
+        if self.egraph.proof_state.proofs_enabled {
+            let merge_idx = self.proof_names().merge_fn_idx_constructor.clone();
+            let merge_row = self.proof_names().merge_fn_row_constructor.clone();
+            // Output column: the merge body with constructor nodes minted via `fd-mint`
+            // (each carrying its own pre-order-indexed existence proof), `old`/`new`
+            // projected to the output column.
+            let mut idx = 0usize;
+            let body = self.render_construct_body(merge, true, fname, &merge_idx, &mut idx);
+            // Proof column for f's view row. `MergeRow` reconstructs `f(inputs...,
+            // merged)` by running the whole merge body on the premise outputs.
+            // For saturation: if the merged value equals a premise output, keep that
+            // premise's existing proof (so the surviving row is identical); otherwise
+            // mint a fresh `MergeRow`. Comparison is over the output column.
+            let out_value = Self::render_merge_on_pair_first(merge);
+            let fresh = format!("({merge_row} \"{fname}\" (pair-second old) (pair-second new))");
+            let proof = format!(
+                "(select-eq {out_value} (pair-first old) (pair-second old) \
+                  (select-eq {out_value} (pair-first new) (pair-second new) {fresh}))"
+            );
+            format!("(pair {body} {proof})")
+        } else {
+            // Term mode (no proofs): the view value is the output directly, but the
+            // constructors must still be minted into their FD views (a plain `(C a b)`
+            // call creates the term but not the view row lookups consult), so wrap
+            // each in `fd-mint` with no proof.
+            let mut idx = 0usize;
+            self.render_construct_body(merge, false, fname, "", &mut idx)
+        }
+    }
+
+    /// Render a constructor-bodied merge body for the output column of a Phase B FD
+    /// view's `:merge`. Constructor calls become `(fd-mint (C ...) [proof])`, minting
+    /// `C` into its FD view and returning the output e-class.
+    ///
+    /// In proof mode each node carries `MergeIdx(fname, (pair-second old),
+    /// (pair-second new), idx)` (idx = pre-order position, matching `subexpr_at_index`
+    /// in the checker) and `old`/`new` project via `pair-first`. In term mode there is
+    /// no proof and `old`/`new` stay bare. `idx` is threaded for distinct indices.
+    fn render_construct_body(
         &mut self,
-        fdecl: &ResolvedFunctionDecl,
-        child_names: &[String],
-        rebuilding_ruleset: &str,
+        expr: &ResolvedExpr,
+        proofs: bool,
+        fname: &str,
+        merge_idx: &str,
+        idx: &mut usize,
     ) -> String {
-        // Congruence rule
-        let fresh_name = self.egraph.parser.symbol_gen.fresh("congruence_rule");
-        let mut child_names_new = child_names.to_vec();
-        child_names_new.push("new".to_string());
-        let mut child_names_old = child_names.to_vec();
-        child_names_old.push("old".to_string());
-        let (query1, prf1) = self.query_view_and_get_proof(&fdecl.name, &child_names_new);
-        let (query2, prf2) = self.query_view_and_get_proof(&fdecl.name, &child_names_old);
-        let sym = &self.proof_names().eq_sym_constructor;
-        let trans = &self.proof_names().eq_trans_constructor;
-
-        // Proof is by transitivity. A view proof gives a proof that
-        // representative r_1 = f(c_1,...,c_n).
-        // We also have a proof that other eclass representative r_2 = f(c_1,...,c_n), the same term.
-        // We want a proof that r1 = r2, which we get by transitivity.
-        let union_code = self.union(
-            &fdecl.schema.output,
-            "new",
-            "old",
-            &Justification::Proof(format!("({trans} {prf1} ({sym} {prf2}))",)),
-        );
-        // Action-side term construction can create a fresh visible view row for
-        // child tuples that were already subsumed. Congruence maintenance still
-        // has to see those subsumed rows so it can union the old and new outputs.
-        format!(
-            "(rule ({query1}
-                        {query2}
-                        (!= old new)
-                        (= (ordering-max old new) new))
-                       ({union_code})
-                        :ruleset {rebuilding_ruleset}
-                        :internal-include-subsumed
-                        :name \"{fresh_name}\")"
-        )
+        let my_idx = *idx;
+        *idx += 1;
+        match expr {
+            ResolvedExpr::Lit(_, lit) => format!("{lit}"),
+            ResolvedExpr::Var(_, var) => {
+                let n = var.name.as_str();
+                if proofs && (n == "old" || n == "new") {
+                    format!("(pair-first {n})")
+                } else {
+                    n.to_string()
+                }
+            }
+            ResolvedExpr::Call(_, ResolvedCall::Func(c), args) => {
+                // A constructor node: mint it via `fd-mint`, carrying its own
+                // existence proof (indexed by its pre-order position) in proof mode.
+                // The FD view name is emitted as a string literal so the desugared
+                // program is self-contained (it does not depend on the encoder's
+                // runtime view-name map when re-parsed).
+                let view_name = self.view_name(&c.name);
+                let rendered: Vec<String> = args
+                    .iter()
+                    .map(|a| self.render_construct_body(a, proofs, fname, merge_idx, idx))
+                    .collect();
+                let ctor_call = format!("({} {})", c.name, ListDisplay(rendered, " "));
+                if proofs {
+                    let node_proof = format!(
+                        "({merge_idx} \"{fname}\" (pair-second old) (pair-second new) {my_idx})"
+                    );
+                    format!("(fd-mint \"{view_name}\" {ctor_call} {node_proof})")
+                } else {
+                    format!("(fd-mint \"{view_name}\" {ctor_call})")
+                }
+            }
+            ResolvedExpr::Call(_, ResolvedCall::Primitive(p), args) => {
+                let rendered: Vec<String> = args
+                    .iter()
+                    .map(|a| self.render_construct_body(a, proofs, fname, merge_idx, idx))
+                    .collect();
+                format!("({} {})", p.name(), ListDisplay(rendered, " "))
+            }
+        }
     }
 
-    /// Generate rules that handle merge functions or congruence.
-    /// For custom functions, we generate rules that run the merge function.
-    /// For constructors, we generate congruence rules.
-    fn handle_merge_or_congruence(&mut self, fdecl: &ResolvedFunctionDecl) -> String {
-        let child_names = fdecl
-            .schema
-            .input
-            .iter()
-            .enumerate()
-            .map(|(i, _)| format!("c{i}_"))
-            .collect::<Vec<_>>();
-        let child_names_str = child_names.join(" ");
-        let rebuilding_ruleset = self.proof_names().rebuilding_ruleset_name.clone();
-        let view_name = self.view_name(&fdecl.name);
-        if fdecl.subtype == FunctionSubtype::Custom {
-            self.handle_merge_fn(
-                fdecl,
-                &child_names,
-                &child_names_str,
-                &view_name,
-                &rebuilding_ruleset,
-            )
-        } else {
-            self.handle_congruence(fdecl, &child_names, &rebuilding_ruleset)
+    /// Render a resolved merge body to egglog source, replacing the bare leaf vars
+    /// `old`/`new` with `(pair-first old)`/`(pair-first new)` (the output column of the
+    /// pair-view value).
+    fn render_merge_on_pair_first(expr: &ResolvedExpr) -> String {
+        Self::render_merge_expr(expr, true)
+    }
+
+    /// Render a resolved merge body to egglog source as-is (term mode: the view value
+    /// is the output directly, so `old`/`new` stay bare).
+    fn render_merge_on_old_new(expr: &ResolvedExpr) -> String {
+        Self::render_merge_expr(expr, false)
+    }
+
+    fn render_merge_expr(expr: &ResolvedExpr, project_first: bool) -> String {
+        match expr {
+            ResolvedExpr::Lit(_, lit) => format!("{lit}"),
+            ResolvedExpr::Var(_, var) => {
+                let n = var.name.as_str();
+                if project_first && (n == "old" || n == "new") {
+                    format!("(pair-first {n})")
+                } else {
+                    n.to_string()
+                }
+            }
+            ResolvedExpr::Call(_, call, args) => {
+                let rendered: Vec<String> = args
+                    .iter()
+                    .map(|a| Self::render_merge_expr(a, project_first))
+                    .collect();
+                format!("({} {})", call.name(), ListDisplay(rendered, " "))
+            }
         }
     }
 
@@ -418,6 +654,15 @@ impl<'a> ProofInstrumentor<'a> {
         let schema = &fdecl.schema;
         let out_type = schema.output.clone();
 
+        let is_fd = self.is_fd_pair_view(fdecl);
+        let is_fd_custom = is_fd && fdecl.subtype == FunctionSubtype::Custom;
+        if is_fd {
+            self.egraph
+                .proof_state
+                .fd_view_funcs
+                .insert(fdecl.name.clone());
+        }
+
         let name = &fdecl.name;
         let view_name = self.view_name(&fdecl.name);
         let in_sorts = ListDisplay(schema.input.clone(), " ");
@@ -458,7 +703,8 @@ impl<'a> ProofInstrumentor<'a> {
         if let Some(cost) = fdecl.cost {
             term_flags.push_str(&format!(" :cost {cost}"));
         }
-        // View is always a function (returning Proof or Unit), with :merge old
+        // The view is always a function; its `:merge` does congruence (constructors)
+        // or value-replacement / primitive / constructor-bodied merging (customs).
         let proof_type = self.proof_type_str().to_string();
         let mut view_flags = String::new();
         if fdecl.unextractable {
@@ -470,12 +716,82 @@ impl<'a> ProofInstrumentor<'a> {
         if fdecl.internal_let {
             view_flags.push_str(" :internal-let");
         }
-        let view_decl = format!(
-            "(function {view_name} ({view_sorts}) {proof_type} :merge old :internal-term-constructor {name}{view_flags})"
-        );
+        // For an FD custom view the output column's pair sort `(Pair output proof)`
+        // is not declared by `declare_sort` (the output is typically a non-eq-sort
+        // like i64/Set, which has no UF setup), so declare it here.
+        let mut extra_pair_sort_decl = String::new();
+        let view_decl = if fdecl.subtype == FunctionSubtype::Constructor {
+            // FD view: key is the children only. In term mode the value is the
+            // output (the eclass representative), a plain eq-sort kept indexable
+            // for cheap rebuild canonicalization. In proof mode the value is a
+            // `(pair output proof)` (two value columns): the output stays a real
+            // eq-sort column (fast rebuild) while the per-row existence proof
+            // rides alongside it. Congruence is handled by `:merge`, which reads
+            // both rows' proofs from the pair.
+            let ctor_merge = self.constructor_view_merge(&out_type);
+            let view_value_sort = if self.egraph.proof_state.proofs_enabled {
+                self.uf_pair_sort_name(&out_type)
+            } else {
+                out_type.clone()
+            };
+            format!(
+                "(function {view_name} ({in_sorts}) {view_value_sort} :merge {ctor_merge} :internal-term-constructor {name} :identity-values 1{view_flags})"
+            )
+        } else if is_fd_custom {
+            // Custom function on the FD pair-valued view: key is the children only,
+            // value is `(pair output proof)` in proof mode (output only in term mode).
+            // The user's `:merge` runs on the output column. No union: the output is a
+            // merged value, not an eclass collision.
+            //
+            // Primitive-bodied merges (`min`/`or`/...) render directly; constructor-
+            // bodied merges (Phase B, e.g. `(C2 (C1 old new) ...)`) mint each
+            // constructor node via the `fd-mint` Construct surface form. Both carry a
+            // `MergeRow` justification on the f-view proof column.
+            let merge = fdecl
+                .merge
+                .as_ref()
+                .expect("FD custom view requires a :merge");
+            let custom_merge = if self.is_constructor_bodied_fd_custom(fdecl) {
+                self.constructor_bodied_fd_view_merge(&fdecl.name.clone(), merge)
+            } else {
+                self.custom_fd_view_merge(&fdecl.name.clone(), merge)
+            };
+            let view_value_sort = if self.egraph.proof_state.proofs_enabled {
+                // Only emit the `(sort ...)` declaration the first time we mint the
+                // pair sort for this output sort (another FD custom function with the
+                // same output sort would otherwise re-declare it).
+                let already_declared = self
+                    .egraph
+                    .proof_state
+                    .uf_pair_sort
+                    .contains_key(out_type.as_str());
+                let pair_sort = self.uf_pair_sort_name(&out_type);
+                if !already_declared {
+                    let proof_type = self.proof_type_str().to_string();
+                    extra_pair_sort_decl =
+                        format!("(sort {pair_sort} (Pair {out_type} {proof_type}))");
+                }
+                pair_sort
+            } else {
+                out_type.clone()
+            };
+            format!(
+                "(function {view_name} ({in_sorts}) {view_value_sort} :merge {custom_merge} :internal-term-constructor {name} :identity-values 1{view_flags})"
+            )
+        } else {
+            // A custom function that is neither a constructor nor FD would have
+            // already tripped the `unreachable!` in `handle_merge_or_congruence`
+            // above (called before this `view_decl` is built), so this branch is
+            // dead: every proof-supported custom merge is FD.
+            let _ = (&view_sorts, &proof_type);
+            unreachable!(
+                "non-FD custom merge in a proof-supported program (see handle_merge_or_congruence)"
+            )
+        };
         self.parse_program(&format!(
             "
             (sort {fresh_sort})
+            {extra_pair_sort_decl}
             {to_ast_view_sort}
             (constructor {name} ({term_sorts}) {view_sort}{term_flags} :internal-hidden :unextractable)
             {view_decl}
@@ -502,9 +818,17 @@ impl<'a> ProofInstrumentor<'a> {
         }
 
         let view_name = self.view_name(&fdecl.name);
+        // FD views (constructors + primitive-bodied customs) key on the children only
+        // (the output lives in the value column); legacy custom views key on all
+        // columns (the output is part of the key).
+        let is_fd = self.is_fd_pair_view(fdecl);
         let child = |i: usize| format!("c{i}_");
         let children_vec: Vec<String> = (0..types.len()).map(child).collect();
-        let children = format!("{}", ListDisplay(&children_vec, " "));
+        let delete_key = if is_fd {
+            ListDisplay(&children_vec[..children_vec.len() - 1], " ").to_string()
+        } else {
+            ListDisplay(&children_vec, " ").to_string()
+        };
 
         // For each eq-sort column, look up its leader via the UF table.
         // For non-eq-sort columns, the leader is the same as the original.
@@ -549,7 +873,8 @@ impl<'a> ProofInstrumentor<'a> {
         let children_updated: Vec<String> = leader_vars.clone();
 
         let fresh_name = self.egraph.parser.symbol_gen.fresh("rebuild_rule");
-        let (query_view, view_prf) = self.query_view_and_get_proof(&fdecl.name, &children_vec);
+        let (query_view, view_prf) =
+            self.query_view_and_get_proof(&fdecl.name, &children_vec, is_fd, &fdecl.schema.output);
 
         // Build proof code if proofs are enabled.
         // We chain congruence proofs for each updated child and a transitivity proof
@@ -599,7 +924,13 @@ impl<'a> ProofInstrumentor<'a> {
             ("".to_string(), "()".to_string())
         };
 
-        let updated_view = self.update_view(&fdecl.name, &children_updated, &pf_var);
+        let updated_view = self.update_view(
+            &fdecl.name,
+            &children_updated,
+            &pf_var,
+            is_fd,
+            &fdecl.schema.output,
+        );
 
         // Make a single rule that updates the view when any child's leader differs.
         let rule = format!(
@@ -610,7 +941,7 @@ impl<'a> ProofInstrumentor<'a> {
                  (
                   {pf_code}
                   {updated_view}
-                  (delete ({view_name} {children}))
+                  (delete ({view_name} {delete_key}))
                  )
                   :ruleset {} :name \"{fresh_name}\" :internal-include-subsumed)",
             self.proof_names().rebuilding_ruleset_name
@@ -728,17 +1059,40 @@ impl<'a> ProofInstrumentor<'a> {
                     new_args.push(var);
                     arg_proofs.push(proof);
                 }
-                new_args.push(v.to_string());
 
                 let view_name = self.view_name(head.name());
-                let args_str = ListDisplay(new_args, " ");
-
-                // View is always a function; query it and bind the output
-                let proof_var = self.fresh_var();
-                res.push(format!("(= {proof_var} ({view_name} {args_str}))"));
+                let is_fd = self.name_is_fd_pair_view(head.name());
+
+                // Query the view and obtain the base existence proof. For an FD custom
+                // view the key is the children only and the value is `(pair output
+                // proof)`: bind the output via `pair-first` and source the proof from
+                // `pair-second`. For the legacy view the output `v` is part of the key
+                // and the value IS the proof.
+                let base_proof = if is_fd {
+                    let key_str = ListDisplay(&new_args, " ");
+                    if self.egraph.proof_state.proofs_enabled {
+                        let pair_var = self.fresh_var();
+                        res.push(format!("(= {pair_var} ({view_name} {key_str}))"));
+                        res.push(format!("(= {v} (pair-first {pair_var}))"));
+                        format!("(pair-second {pair_var})")
+                    } else {
+                        res.push(format!("(= {v} ({view_name} {key_str}))"));
+                        "()".to_string()
+                    }
+                } else {
+                    new_args.push(v.to_string());
+                    let args_str = ListDisplay(&new_args, " ");
+                    let proof_var = self.fresh_var();
+                    res.push(format!("(= {proof_var} ({view_name} {args_str}))"));
+                    if self.egraph.proof_state.proofs_enabled {
+                        proof_var
+                    } else {
+                        "()".to_string()
+                    }
+                };
 
                 if self.egraph.proof_state.proofs_enabled {
-                    let mut proof = proof_var;
+                    let mut proof = base_proof;
                     for (i, arg_proof) in arg_proofs.into_iter().enumerate() {
                         let congr = &self.proof_names().congr_constructor;
                         proof = format!(
@@ -804,13 +1158,10 @@ impl<'a> ProofInstrumentor<'a> {
                     } else if resolved_var.sort.is_eq_sort() {
                         let term_proof_name = self.term_proof_name(resolved_var.sort.name());
                         let fresh_proof = self.fresh_var();
-                        // Every eq-sort term has its term_proof set at
-                        // constructor-creation time, so this proof is guaranteed
-                        // present when the rule fires. Fetch it directly in the
-                        // action (the rule is then `:unsafe-seminaive`, see
-                        // instrument_rule) instead of as a body join — one fewer
-                        // join per eq-sort body variable. Callers that don't
-                        // build a proof (run :until, check) discard these.
+                        // An eq-sort term's term_proof is always present when the rule
+                        // fires, so fetch it in the action (making the rule
+                        // `:unsafe-seminaive`, see instrument_rule) rather than as a
+                        // body join — one fewer join per eq-sort body variable.
                         action_lookups
                             .push(format!("(let {fresh_proof} ({term_proof_name} {var}))"));
                         fresh_proof
@@ -851,28 +1202,30 @@ impl<'a> ProofInstrumentor<'a> {
                         let view_name = self.view_name(&func_type.name);
                         let args_str = ListDisplay(new_args, " ");
 
-                        let proof = {
-                            // View is always a function; query it and bind the output
-                            let view_proof_var = self.fresh_var();
-                            res.push(format!(
-                                "(= {view_proof_var} ({view_name} {args_str} {fv}))"
-                            ));
-                            if self.proofs_enabled() {
-                                let mut proof = view_proof_var;
-                                for (i, arg_proof) in arg_proofs.into_iter().enumerate() {
-                                    if let Some(arg_proof) = arg_proof {
-                                        let congr = &self.proof_names().congr_constructor;
-                                        proof = format!(
-                                            "
+                        // FD view: key is the children, value is a
+                        // `(pair output proof)` in proof mode (output only in
+                        // term mode). Bind the output (pair-first) and source
+                        // the existence proof from pair-second.
+                        let proof = if self.proofs_enabled() {
+                            let pair_var = self.fresh_var();
+                            res.push(format!("(= {pair_var} ({view_name} {args_str}))"));
+                            res.push(format!("(= {fv} (pair-first {pair_var}))"));
+                            let tp_var = format!("(pair-second {pair_var})");
+                            let mut proof = tp_var;
+                            for (i, arg_proof) in arg_proofs.into_iter().enumerate() {
+                                if let Some(arg_proof) = arg_proof {
+                                    let congr = &self.proof_names().congr_constructor;
+                                    proof = format!(
+                                        "
                             ({congr} {proof} {i} {arg_proof})
                             "
-                                        );
-                                    }
+                                    );
                                 }
-                                proof
-                            } else {
-                                "()".to_string()
                             }
+                            proof
+                        } else {
+                            res.push(format!("(= {fv} ({view_name} {args_str}))"));
+                            "()".to_string()
                         };
                         (fv, proof)
                     }
@@ -908,13 +1261,11 @@ impl<'a> ProofInstrumentor<'a> {
         }
     }
 
-    /// Return the instrumented query and a proof that it matched.
-    /// Returns `(body_facts, action_lookups, proof)`. Eq-sort variables'
-    /// `term_proof` fetches are emitted into `action_lookups` as
-    /// `(let p (term_proof v))` lines for the caller to splice into the
-    /// rule's actions (the rule is then `:unsafe-seminaive`). Callers
-    /// that don't build a proof (`run :until`, `check`) discard the
-    /// lookups and the proof.
+    /// Return the instrumented query and a proof that it matched, as
+    /// `(body_facts, action_lookups, proof)`. Eq-sort variables' `term_proof`
+    /// fetches go into `action_lookups` for the caller to splice into the rule's
+    /// actions (making the rule `:unsafe-seminaive`); callers that don't build a
+    /// proof (`run :until`, `check`) discard them.
     fn instrument_facts(&mut self, facts: &[ResolvedFact]) -> (Vec<String>, Vec<String>, String) {
         let mut res = vec![];
         let mut action_lookups = vec![];
@@ -995,11 +1346,52 @@ impl<'a> ProofInstrumentor<'a> {
     }
 
     /// Update the view with the given arguments.
-    /// The arguments include the eclass for constructors.
-    /// View is always a function (returning Proof or Unit).
-    fn update_view(&mut self, fname: &str, args: &[String], proof: &str) -> String {
+    ///
+    /// Legacy custom functions key on `args` (children + output) with value `proof`.
+    /// FD views key on the children, with value `(pair output proof)`; for an eq-sort
+    /// output we also record `term_proof(output) = proof` (the eclass's existence
+    /// proof), skipped for non-eq-sort outputs which have no `term_proof` table.
+    fn update_view(
+        &mut self,
+        fname: &str,
+        args: &[String],
+        proof: &str,
+        is_fd: bool,
+        out_sort: &str,
+    ) -> String {
         let view_name = self.view_name(fname);
-        format!("(set ({view_name} {}) {proof})", ListDisplay(args, " "))
+        if is_fd {
+            let (output, key) = args.split_last().expect("FD view needs an output");
+            let key = ListDisplay(key, " ");
+            if self.egraph.proof_state.proofs_enabled {
+                // The value is `(pair output proof)`. For an eq-sort output also record
+                // `term_proof(output) = proof` (used for bare eq-sort vars in facts and
+                // by prove-exists); non-eq-sort outputs have no `term_proof` table.
+                if self.sort_has_term_proof(out_sort) {
+                    let tp = self.term_proof_name(out_sort);
+                    format!(
+                        "(set ({view_name} {key}) (pair {output} {proof}))\n(set ({tp} {output}) {proof})"
+                    )
+                } else {
+                    format!("(set ({view_name} {key}) (pair {output} {proof}))")
+                }
+            } else {
+                format!("(set ({view_name} {key}) {output})")
+            }
+        } else {
+            format!("(set ({view_name} {}) {proof})", ListDisplay(args, " "))
+        }
+    }
+
+    /// Whether a `term_proof` table exists for `sort_name`. These tables are created
+    /// by `declare_sort` for every user-declared eq-sort, so a `term_proof` table
+    /// exists iff we have minted a `term_proof_name` for the sort.
+    fn sort_has_term_proof(&self, sort_name: &str) -> bool {
+        self.egraph
+            .proof_state
+            .proof_names
+            .term_proof_name
+            .contains_key(sort_name)
     }
 
     /// Return some code adding to the view and term tables.
@@ -1046,35 +1438,31 @@ impl<'a> ProofInstrumentor<'a> {
                 Justification::Fiat => {
                     format!("({fiat_constructor} ({to_ast} {fv}) ({to_ast} {fv}))",)
                 }
-                Justification::Merge(fn_name, p1, p2) => {
-                    let merge_constructor = &self.proof_names().merge_fn_constructor;
-                    format!("({merge_constructor} \"{fn_name}\" {p1} {p2} ({to_ast} {fv}))",)
-                }
                 Justification::Proof(existing_proof) => existing_proof.clone(),
             };
 
             let proof_var = self.fresh_var();
-            // add a proof for the constructor if needed
-            let term_proof = if func_type.subtype == FunctionSubtype::Constructor {
-                let term_proof_constructor = self.term_proof_name(func_type.output.name());
-                format!("(set ({term_proof_constructor} {fv}) {proof_var})")
-            } else {
-                "".to_string()
-            };
-
-            (
-                format!(
-                    "(let {proof_var} {proof})
-                     {term_proof}"
-                ),
-                proof_var,
-            )
+            // For constructors, `term_proof(output) = proof` is written by
+            // `update_view` (single source of truth for the FD view + its
+            // proof). For custom functions there is no term_proof entry.
+            (format!("(let {proof_var} {proof})"), proof_var)
         } else {
             ("".to_string(), "()".to_string())
         };
 
         res.push(proof_str);
-        res.push(self.update_view(&func_type.name, &args_with_fv, &view_proof_var));
+        // FD functions (constructors + primitive-bodied customs) use the pair-valued
+        // view keyed on children only. For constructors `args_with_fv` appended the
+        // freshly-minted eclass `fv` as the output; for FD customs `args` already
+        // ends with the output value (from the `(set (f c..) v)` action).
+        let is_fd = self.func_type_is_fd_pair_view(func_type);
+        res.push(self.update_view(
+            &func_type.name,
+            &args_with_fv,
+            &view_proof_var,
+            is_fd,
+            func_type.output.name(),
+        ));
 
         // add to uf table to initialize eclass for constructors
         if func_type.subtype == FunctionSubtype::Constructor {
@@ -1089,13 +1477,43 @@ impl<'a> ProofInstrumentor<'a> {
         (res, fv)
     }
 
-    /// Returns a query for (fname args) and a variable for the proof (or Unit) output.
-    /// View is always a function, so we always use `(= var (view ...))` form.
-    fn query_view_and_get_proof(&mut self, fname: &str, args: &[String]) -> (String, String) {
+    /// Returns a query binding the view's value and a variable for the proof
+    /// (or Unit) output.
+    ///
+    /// Legacy custom functions take the full key in `args` with the proof as value.
+    /// FD-shape constructors take the output as the last `args` element (bound from
+    /// the view value) and the rest as key; in proof mode the value is a
+    /// `(pair output proof)`, so bind via `pair-first` and return `pair-second`.
+    fn query_view_and_get_proof(
+        &mut self,
+        fname: &str,
+        args: &[String],
+        is_fd: bool,
+        out_sort: &str,
+    ) -> (String, String) {
+        let _ = out_sort;
         let view_name = self.view_name(fname);
-        let pf_var = self.fresh_var();
-        let query = format!("(= {pf_var} ({view_name} {}))", ListDisplay(args, " "));
-        (query, pf_var)
+        if is_fd {
+            let (output, key) = args.split_last().expect("FD view needs an output");
+            let key = ListDisplay(key, " ");
+            if self.egraph.proof_state.proofs_enabled {
+                // The FD view value is a `(pair output proof)`; bind the pair,
+                // then project the output and proof out of it.
+                let pair_var = self.fresh_var();
+                let pf_var = format!("(pair-second {pair_var})");
+                let query = format!(
+                    "(= {pair_var} ({view_name} {key}))\n(= {output} (pair-first {pair_var}))"
+                );
+                (query, pf_var)
+            } else {
+                let query = format!("(= {output} ({view_name} {key}))");
+                (query, "()".to_string())
+            }
+        } else {
+            let pf_var = self.fresh_var();
+            let query = format!("(= {pf_var} ({view_name} {}))", ListDisplay(args, " "));
+            (query, pf_var)
+        }
     }
 
     // Add to view and term tables, returning a variable for the created term.
@@ -1217,16 +1635,17 @@ impl<'a> ProofInstrumentor<'a> {
     /// Any schedule should be sound as long as we saturate.
     fn rebuild(&mut self) -> Schedule {
         let path_compress_ruleset = self.proof_names().path_compress_ruleset_name.clone();
-        let single_parent = self.proof_names().single_parent_ruleset_name.clone();
         let uf_function_index = self.proof_names().uf_function_index_ruleset_name.clone();
         let rebuilding_cleanup_ruleset = self.proof_names().rebuilding_cleanup_ruleset_name.clone();
         let rebuilding_ruleset = self.proof_names().rebuilding_ruleset_name.clone();
         let delete_ruleset = self.proof_names().delete_subsume_ruleset_name.clone();
+        // The single-parent invariant is now maintained by the UF function index's
+        // `:merge` (a source with two parents collides on the index key), so there is
+        // no separate `single_parent` ruleset to saturate here.
         self.parse_schedule(format!(
             "(seq
               (saturate
                   {rebuilding_cleanup_ruleset}
-                  (saturate {single_parent})
                   (saturate {path_compress_ruleset})
                   (saturate {uf_function_index})
                   {rebuilding_ruleset})
@@ -1355,12 +1774,7 @@ impl<'a> ProofInstrumentor<'a> {
             ResolvedNCommand::PrintSize(span, name) => {
                 // In proof mode, print the size of the view table for constructors
                 let new_name = name.as_ref().map(|n| {
-                    if self
-                        .egraph
-                        .type_info
-                        .get_func_type(n)
-                        .is_some_and(|f| f.subtype == FunctionSubtype::Constructor)
-                    {
+                    if self.name_is_fd_pair_view(n) {
                         self.view_name(n)
                     } else {
                         n.clone()
diff --git a/src/proofs/proof_encoding_helpers.rs b/src/proofs/proof_encoding_helpers.rs
index 0491e94fa..d65187de1 100644
--- a/src/proofs/proof_encoding_helpers.rs
+++ b/src/proofs/proof_encoding_helpers.rs
@@ -24,13 +24,24 @@ pub(crate) struct EncodingNames {
     pub(crate) fiat_constructor: String,
     pub(crate) rule_constructor: String,
     pub(crate) merge_fn_constructor: String,
+    /// Index-carrying term-free merge justification `(name p_old p_new idx)`. The
+    /// conclusion is reconstructed during proof conversion from the two premise proofs
+    /// and subexpression `idx` of the merge body (a pre-order index distinguishing
+    /// nested subexpressions that share the same premises). Used by the FD
+    /// custom-function view merge, which runs without the children.
+    pub(crate) merge_fn_idx_constructor: String,
+    /// Term-free merge justification `(name p_old p_new)` for the FD view row
+    /// `f(children) = eval(whole merge body)`. Unlike `merge_fn_idx_constructor`
+    /// (which proves a particular nested subterm), this proves the function's own view
+    /// row, so it carries no index. Emitted as the proof column of every FD view's
+    /// `:merge`.
+    pub(crate) merge_fn_row_constructor: String,
     pub(crate) eq_trans_constructor: String,
     pub(crate) eq_sym_constructor: String,
     pub(crate) congr_constructor: String,
     /// For a given function symbol, the name of the function that converts to the AST type.
     pub(crate) sort_to_ast_constructor: HashMap<String, String>,
     pub(crate) fn_to_term_sort: HashMap<String, String>,
-    pub(crate) single_parent_ruleset_name: String,
     pub(crate) uf_function_index_ruleset_name: String,
     pub(crate) pcons: String,
     pub(crate) pnil: String,
@@ -52,8 +63,7 @@ pub(crate) struct EncodingNames {
 pub(crate) enum Justification {
     Rule(String, String), // rule name and proof list
     Fiat,
-    Proof(String),                 // existing proof
-    Merge(String, String, String), // function name, proof1, proof2
+    Proof(String), // existing proof
 }
 
 impl EncodingNames {
@@ -65,12 +75,13 @@ impl EncodingNames {
             fiat_constructor: symbol_gen.fresh("Fiat"),
             rule_constructor: symbol_gen.fresh("Rule"),
             merge_fn_constructor: symbol_gen.fresh("Merge"),
+            merge_fn_idx_constructor: symbol_gen.fresh("MergeIdx"),
+            merge_fn_row_constructor: symbol_gen.fresh("MergeRow"),
             eq_trans_constructor: symbol_gen.fresh("Trans"),
             eq_sym_constructor: symbol_gen.fresh("Sym"),
             congr_constructor: symbol_gen.fresh("Congr"),
             sort_to_ast_constructor: HashMap::default(),
             fn_to_term_sort: HashMap::default(),
-            single_parent_ruleset_name: symbol_gen.fresh("single_parent"),
             uf_function_index_ruleset_name: symbol_gen.fresh("uf_function_index"),
             pcons: symbol_gen.fresh("PCons"),
             pnil: symbol_gen.fresh("PNil"),
@@ -116,10 +127,20 @@ impl ProofInstrumentor<'_> {
     /// Returns the name of the Pair sort used to bundle (leader, proof) in the UF function index.
     /// Only used in proof mode.
     pub(crate) fn uf_pair_sort_name(&mut self, sort: &str) -> String {
-        self.egraph
-            .parser
-            .symbol_gen
-            .fresh(&format!("UFPair_{sort}"))
+        if let Some(name) = self.egraph.proof_state.uf_pair_sort.get(sort) {
+            name.clone()
+        } else {
+            let fresh_name = self
+                .egraph
+                .parser
+                .symbol_gen
+                .fresh(&format!("UFPair_{sort}"));
+            self.egraph
+                .proof_state
+                .uf_pair_sort
+                .insert(sort.to_string(), fresh_name.clone());
+            fresh_name
+        }
     }
 
     pub(crate) fn parse_program(&mut self, input: &str) -> Vec<Command> {
@@ -148,10 +169,8 @@ impl ProofInstrumentor<'_> {
              (ruleset {})
              (ruleset {})
              (ruleset {})
-             (ruleset {})
              (ruleset {})",
             self.proof_names().path_compress_ruleset_name,
-            self.proof_names().single_parent_ruleset_name,
             self.proof_names().uf_function_index_ruleset_name,
             self.proof_names().rebuilding_ruleset_name,
             self.proof_names().rebuilding_cleanup_ruleset_name,
@@ -360,6 +379,8 @@ impl ProofInstrumentor<'_> {
             ref fiat_constructor,
             ref rule_constructor,
             ref merge_fn_constructor,
+            ref merge_fn_idx_constructor,
+            ref merge_fn_row_constructor,
             ref eq_trans_constructor,
             ref eq_sym_constructor,
             ref congr_constructor,
@@ -388,6 +409,19 @@ impl ProofInstrumentor<'_> {
 ;; and the proposition being justified t = t
 (constructor {merge_fn_constructor} (String {proof_datatype} {proof_datatype} {ast_sort}) {proof_datatype} :internal-hidden)
 
+;; index-carrying term-free merge function justification- name of function, two premise
+;; proofs, and a pre-order index identifying which subexpression of the merge body this
+;; proof is for. The conclusion term is reconstructed during proof conversion (from the
+;; premises + evaluating subexpression idx of the merge body), so it is not stored here.
+;; Used by the FD custom-function view merge.
+(constructor {merge_fn_idx_constructor} (String {proof_datatype} {proof_datatype} i64) {proof_datatype} :internal-hidden)
+
+;; term-free merge function justification for the FD VIEW ROW- name of function and the
+;; two premise proofs (the colliding view rows). The conclusion `f(children) = eval(body)`
+;; is reconstructed during proof conversion by running the WHOLE merge body on the premise
+;; outputs. Used as the proof column of every FD pair-valued view's :merge.
+(constructor {merge_fn_row_constructor} (String {proof_datatype} {proof_datatype}) {proof_datatype} :internal-hidden)
+
 ;; transitivity of equality proofs
 (constructor {eq_trans_constructor} ({proof_datatype} {proof_datatype}) {proof_datatype} :internal-hidden)
 
diff --git a/src/proofs/proof_format.rs b/src/proofs/proof_format.rs
index 027e2dfbd..b9b212ab4 100644
--- a/src/proofs/proof_format.rs
+++ b/src/proofs/proof_format.rs
@@ -1,7 +1,10 @@
 use crate::{
     ResolvedCall, Term, TermDag, TermId,
     ast::{FunctionSubtype, ResolvedExpr, ResolvedFact, ResolvedNCommand},
-    proofs::{proof_checker::gather_globals, proof_encoding_helpers::EncodingNames},
+    proofs::{
+        proof_checker::{gather_globals, run_merge, run_merge_subexpr},
+        proof_encoding_helpers::EncodingNames,
+    },
     typechecking::FuncType,
     util::{HEntry, HashMap, IndexSet, SymbolGen},
 };
@@ -58,6 +61,18 @@ enum RawProof {
     /// of t = t.
     /// The term t is either f(c1, c2, ..., merge_fn) or some subexpression of the merge function. Here the merge function is evaluted on the terms old and new.
     MergeFn(String, RawProofId, RawProofId, TermId),
+    /// Like [`RawProof::MergeFn`] but term-free: instead of an embedded conclusion, the
+    /// index `idx` identifies which subexpression of the merge body this justifies (a
+    /// pre-order index over the body tree). The conclusion is reconstructed during
+    /// conversion by evaluating subexpression `idx` on the premise outputs; the index
+    /// distinguishes nested subexpressions that share the same premises. Used by the
+    /// FD custom-function view merge, which runs without access to children.
+    MergeFnIdx(String, RawProofId, RawProofId, usize),
+    /// Like [`RawProof::MergeFnIdx`] but for the FD view row (no index). The conclusion
+    /// `f(children) = eval(whole merge body)` is reconstructed during conversion by
+    /// running the whole body on the two premise outputs. Used as the proof column of
+    /// every FD pair-valued view's `:merge`.
+    MergeFnRow(String, RawProofId, RawProofId),
     Trans(RawProofId, RawProofId),
     Sym(RawProofId),
     /// given a proof that t1 = f(..., ci, ...)
@@ -214,6 +229,19 @@ impl RawProofStore {
             let name = self.parse_string(args[0]);
             let premises = self.parse_proof_list(args[1]);
             RawProof::Rule(name, premises, args[2], args[3])
+        } else if head.contains("MergeIdx") {
+            assert!(args.len() == 4, "merge-idx constructor should have 4 args");
+            let function = self.parse_string(args[0]);
+            let old_proof = self.parse_proof(args[1]);
+            let new_proof = self.parse_proof(args[2]);
+            let idx = self.parse_index(args[3]);
+            RawProof::MergeFnIdx(function, old_proof, new_proof, idx)
+        } else if head.contains("MergeRow") {
+            assert!(args.len() == 3, "merge-row constructor should have 3 args");
+            let function = self.parse_string(args[0]);
+            let old_proof = self.parse_proof(args[1]);
+            let new_proof = self.parse_proof(args[2]);
+            RawProof::MergeFnRow(function, old_proof, new_proof)
         } else if head.contains("Merge") {
             assert!(args.len() == 4, "merge constructor should have 4 args");
             let function = self.parse_string(args[0]);
@@ -351,6 +379,32 @@ impl ProofStore {
         (store, proof_id)
     }
 
+    /// Reflexivize a (possibly non-reflexive) proof so it can serve as a `MergeFn`
+    /// premise (the checker requires premises to be reflexive, `lhs == rhs`). For
+    /// `p : A = B` returns a proof of `B = B` as `Trans(Sym(p), p)`; an already-
+    /// reflexive `p` is returned unchanged.
+    ///
+    /// This handles eq-sort inputs to FD custom functions: rebuild rewrites the
+    /// view row's proof into a congruence proof `f(orig) = f(canon)`, and
+    /// reflexivizing to its RHS lands both premises on the same canonical view row
+    /// so the checker's input-match succeeds.
+    fn reflexivize_premise(&mut self, premise_id: ProofId) -> ProofId {
+        let prop = self.id_to_proof[premise_id].proposition.clone();
+        if prop.lhs == prop.rhs {
+            return premise_id;
+        }
+        // Sym(p) : rhs = lhs
+        let sym_id = self.id_to_proof.push(Proof {
+            proposition: Proposition::new(prop.rhs, prop.lhs),
+            justification: Justification::Sym(premise_id),
+        });
+        // Trans(Sym(p), p) : rhs = rhs
+        self.id_to_proof.push(Proof {
+            proposition: Proposition::new(prop.rhs, prop.rhs),
+            justification: Justification::Trans(sym_id, premise_id),
+        })
+    }
+
     /// Converts a raw proof into a user-facing proof, recursively converting sub-proofs as needed.
     /// This adds new metadata to the proof, such as the substitution for rules.
     ///
@@ -411,6 +465,106 @@ impl ProofStore {
                     },
                 }
             }
+            RawProof::MergeFnIdx(function, old_raw, new_raw, idx) => {
+                let old_proof_id = self.convert_raw_proof(prog, globals, raw_store, *old_raw);
+                let new_proof_id = self.convert_raw_proof(prog, globals, raw_store, *new_raw);
+                // The two premise proofs are reflexive proofs of the colliding view terms
+                // `f(c..., old_output)` and `f(c..., new_output)`. We extract the two outputs
+                // and reconstruct the conclusion term by evaluating subexpression `idx` of
+                // `function`'s merge body on those outputs (`old`/`new` bound accordingly).
+                //
+                // `idx` indexes all body nodes (pre-order, top node included). The
+                // conclusion is that node's own minted term, i.e. its existence proof in
+                // its FD view. The whole-view-row conclusion comes from `MergeFnRow`.
+                let old_view = self.id_to_proof[old_proof_id].rhs();
+                let new_view = self.id_to_proof[new_proof_id].rhs();
+                let (old_output, new_output) = match (
+                    self.term_dag.get(old_view),
+                    self.term_dag.get(new_view),
+                ) {
+                    (Term::App(_old_head, old_args), Term::App(_new_head, new_args)) => {
+                        let old_output = *old_args.last().expect("merge view term has no args");
+                        let new_output = *new_args.last().expect("merge view term has no args");
+                        (old_output, new_output)
+                    }
+                    _ => panic!(
+                        "MergeFnIdx premise proofs should prove function application terms, got {:?} and {:?}",
+                        self.term_dag.get(old_view),
+                        self.term_dag.get(new_view)
+                    ),
+                };
+                let (subexpr_term, _props) = run_merge_subexpr(
+                    &mut self.term_dag,
+                    function,
+                    prog,
+                    old_output,
+                    new_output,
+                    *idx,
+                )
+                .unwrap_or_else(|e| {
+                    panic!("failed to run merge subexpr {idx} for {function}: {e}")
+                });
+                // The conclusion is that node's own minted term (its existence proof
+                // in its FD view); the whole-view-row conclusion comes from `MergeFnRow`.
+                let to_prove = subexpr_term;
+                // Reflexivize premises in case rebuild rewrote them into congruence
+                // proofs (eq-sort inputs); reflexive premises pass through unchanged.
+                let old_proof_id = self.reflexivize_premise(old_proof_id);
+                let new_proof_id = self.reflexivize_premise(new_proof_id);
+                Proof {
+                    proposition: Proposition::new(to_prove, to_prove),
+                    justification: Justification::MergeFn {
+                        function: function.clone(),
+                        old_proof: old_proof_id,
+                        new_proof: new_proof_id,
+                    },
+                }
+            }
+            RawProof::MergeFnRow(function, old_raw, new_raw) => {
+                let old_proof_id = self.convert_raw_proof(prog, globals, raw_store, *old_raw);
+                let new_proof_id = self.convert_raw_proof(prog, globals, raw_store, *new_raw);
+                // The two premise proofs are reflexive proofs of the colliding view
+                // rows `f(c..., old_output)` and `f(c..., new_output)`. The conclusion
+                // is the whole view row `f(inputs..., merged)`, where `merged` is the
+                // whole merge body evaluated on the two premise outputs.
+                let old_view = self.id_to_proof[old_proof_id].rhs();
+                let new_view = self.id_to_proof[new_proof_id].rhs();
+                let (view_head, input_args, old_output, new_output) = match (
+                    self.term_dag.get(old_view),
+                    self.term_dag.get(new_view),
+                ) {
+                    (Term::App(old_head, old_args), Term::App(_new_head, new_args)) => {
+                        let head = old_head.clone();
+                        let old_output = *old_args.last().expect("merge view term has no args");
+                        let new_output = *new_args.last().expect("merge view term has no args");
+                        let inputs = old_args[..old_args.len() - 1].to_vec();
+                        (head, inputs, old_output, new_output)
+                    }
+                    _ => panic!(
+                        "MergeFnRow premise proofs should prove function application terms, got {:?} and {:?}",
+                        self.term_dag.get(old_view),
+                        self.term_dag.get(new_view)
+                    ),
+                };
+                let (merged_child, _props) =
+                    run_merge(&mut self.term_dag, function, prog, old_output, new_output)
+                        .unwrap_or_else(|e| panic!("failed to run merge for {function}: {e}"));
+                let mut merged_args = input_args;
+                merged_args.push(merged_child);
+                let to_prove = self.term_dag.app(view_head, merged_args);
+                // Reflexivize premises in case rebuild rewrote them into congruence
+                // proofs (eq-sort inputs); reflexive premises pass through unchanged.
+                let old_proof_id = self.reflexivize_premise(old_proof_id);
+                let new_proof_id = self.reflexivize_premise(new_proof_id);
+                Proof {
+                    proposition: Proposition::new(to_prove, to_prove),
+                    justification: Justification::MergeFn {
+                        function: function.clone(),
+                        old_proof: old_proof_id,
+                        new_proof: new_proof_id,
+                    },
+                }
+            }
             RawProof::Trans(left_raw, right_raw) => {
                 let left_id = self.convert_raw_proof(prog, globals, raw_store, *left_raw);
                 let right_id = self.convert_raw_proof(prog, globals, raw_store, *right_raw);
diff --git a/src/proofs/proof_tests.rs b/src/proofs/proof_tests.rs
index dd42eea40..a881be616 100644
--- a/src/proofs/proof_tests.rs
+++ b/src/proofs/proof_tests.rs
@@ -8,10 +8,68 @@ mod tests {
         egraph.resolve_program(None, source).unwrap()
     }
 
-    /// The proof encoder reads body variables' `term_proof`s from the RHS via
-    /// `:unsafe-seminaive` lookups. Assert this produces the same database as
-    /// the safe baseline (the same rules annotated `:naive`), for a hardcoded
-    /// handful of files (running it across all tests would be too slow).
+    fn proof_encode(source: &str) -> String {
+        let mut egraph = crate::EGraph::new_with_proofs();
+        let commands = egraph.resolve_program(None, source).unwrap();
+        sanitize_internal_names(&commands)
+            .iter()
+            .map(|cmd| cmd.to_string())
+            .collect::<Vec<_>>()
+            .join("\n")
+    }
+
+    /// A trivial eq-sort-output custom merge (`:merge old`) routes onto the FD
+    /// pair-valued view: the view carries the `:identity-values` stamp and its
+    /// `:merge` builds a `(pair ...)` value (no legacy `handle_merge_fn` rule).
+    #[test]
+    fn trivial_eq_sort_output_merge_is_fd() {
+        let encoding = proof_encode(
+            r#"
+            (datatype T (A) (B))
+            (function keep (i64) T :merge old)
+            (set (keep 0) (A))
+            (set (keep 0) (B))
+            (check (= (keep 0) (A)))
+            "#,
+        );
+        // The FD view stamps `:identity-values 1` on the generated view function.
+        assert!(
+            encoding.contains(":identity-values"),
+            "trivial eq-sort merge should produce an FD view (got: {encoding})"
+        );
+        // FD merges produce a `(pair ...)` value rather than the legacy
+        // output-in-key `:merge old` view shape with a separate merge rule.
+        assert!(
+            encoding.contains("(pair"),
+            "FD view merge should build a pair value (got: {encoding})"
+        );
+    }
+
+    /// Reading a function in a `:merge` body is rejected at typecheck
+    /// (`LookupInMergeDisallowed`) in all modes — a merge must be a pure write.
+    #[test]
+    fn function_reading_merge_is_rejected() {
+        let source = r#"
+            (function foo () i64 :merge (min old new))
+            (function bar () i64 :merge (foo))
+        "#;
+        // Rejected universally — even in plain (normal) mode.
+        let mut e = crate::EGraph::default();
+        let err = e.resolve_program(None, source);
+        assert!(
+            matches!(
+                err,
+                Err(crate::Error::TypeError(
+                    crate::TypeError::LookupInMergeDisallowed(..)
+                ))
+            ),
+            "expected LookupInMergeDisallowed typecheck error, got {err:?}"
+        );
+    }
+
+    /// The proof encoder reads body variables' `term_proof`s via
+    /// `:unsafe-seminaive` lookups; check this matches the `:naive` baseline
+    /// database, on a hardcoded handful of files (all tests would be too slow).
     #[test]
     fn unsafe_seminaive_matches_naive() {
         let files = [
diff --git a/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snap b/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snap
index de728f721..d41a80cd3 100644
--- a/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snap
+++ b/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snap
@@ -3,71 +3,57 @@ source: src/proofs/proof_tests.rs
 expression: snapshot
 ---
 (ruleset __parent)
-(ruleset __single_parent)
 (ruleset __uf_function_index)
 (ruleset __rebuilding)
 (ruleset __rebuilding_cleanup)
 (ruleset __delete_subsume_ruleset)
 (sort Math :internal-uf __UF_Math)
 (function __UF_Math (Math Math) Unit :merge old :unextractable :internal-hidden)
-(function __UF_Mathf (Math) Math :merge new :unextractable :internal-hidden)
+(function __UF_Mathf (Math) Math :merge ((set (__UF_Math (ordering-max old new) (ordering-min old new)) ()) (ordering-min old new)) :unextractable :internal-hidden)
 (rule ((__UF_Math a b)
        (__UF_Math b c)
        (!= b c))
       ((delete (__UF_Math a b))
        (set (__UF_Math a c) ()))
         :ruleset __parent :name "__uf_update")
-(rule ((__UF_Math a b)
-       (__UF_Math a c)
-       (!= b c)
-       (= (ordering-max b c) b))
-      ((delete (__UF_Math a b))
-       (set (__UF_Math b c) ()))
-        :ruleset __single_parent :name "singleparent__uf_update")
 (rule ((__UF_Math a b))
       ((set (__UF_Mathf a) b))
         :ruleset __uf_function_index :name "__uf_function_index1")
 (sort __view)
 (constructor Add (i64 i64) Math :unextractable :internal-hidden)
-(function __AddView (i64 i64 Math) Unit :merge old :internal-term-constructor Add)
+(function __AddView (i64 i64) Math :merge ((set (__UF_Math (ordering-max old new) (ordering-min old new)) ()) (ordering-min old new)) :internal-term-constructor Add :identity-values 1)
 (constructor __to_delete_Add (i64 i64) __view :internal-hidden)
 (constructor __to_subsume_Add (i64 i64) __view :internal-hidden)
-(rule ((= __v (__AddView c0_ c1_ new))
-       (= __v1 (__AddView c0_ c1_ old))
-       (!= old new)
-       (= (ordering-max old new) new))
-      ((set (__UF_Math (ordering-max new old) (ordering-min new old)) ()))
-        :ruleset __rebuilding :name "__congruence_rule" :internal-include-subsumed)
 (rule ((__to_delete_Add c0_ c1_)
-       (__AddView c0_ c1_ out))
-      ((delete (__AddView c0_ c1_ out))
+       (= out (__AddView c0_ c1_)))
+      ((delete (__AddView c0_ c1_))
        (delete (__to_delete_Add c0_ c1_)))
         :ruleset __delete_subsume_ruleset :name "__delete_rule")
 (rule ((__to_subsume_Add c0_ c1_)
-       (__AddView c0_ c1_ out))
-      ((subsume (__AddView c0_ c1_ out)))
+       (= out (__AddView c0_ c1_)))
+      ((subsume (__AddView c0_ c1_)))
         :ruleset __delete_subsume_ruleset :name "__delete_rule_subsume")
-(rule ((= __v2 (__AddView c0_ c1_ c2_))
+(rule ((= c2_ (__AddView c0_ c1_))
        (= c2_leader_ (__UF_Mathf c2_))
        (guard (or (bool-!= c2_ c2_leader_))))
-      ((set (__AddView c0_ c1_ c2_leader_) ())
-       (delete (__AddView c0_ c1_ c2_)))
+      ((set (__AddView c0_ c1_) c2_leader_)
+       (delete (__AddView c0_ c1_)))
         :ruleset __rebuilding :name "__rebuild_rule" :internal-include-subsumed)
-(function __v3 () Math :no-merge :unextractable :internal-let)
-(set (__v3) (Add 1 2))
-(set (__AddView 1 2 (__v3)) ())
-(set (__UF_Math (ordering-max (__v3) (__v3)) (ordering-min (__v3) (__v3))) ())
-(run-schedule (seq (saturate (seq (run __rebuilding_cleanup) (saturate (run __single_parent)) (saturate (run __parent)) (saturate (run __uf_function_index)) (run __rebuilding))) (run __delete_subsume_ruleset)))
-(rule ((= __v5 (__AddView a b __v4)))
-      ((let __v7 (Add a b))
-       (set (__AddView a b __v7) ())
-       (set (__UF_Math (ordering-max __v7 __v7) (ordering-min __v7 __v7)) ())
-       (let __v8 (Add b a))
-       (set (__AddView b a __v8) ())
-       (set (__UF_Math (ordering-max __v8 __v8) (ordering-min __v8 __v8)) ())
-       (set (__UF_Math (ordering-max __v7 __v8) (ordering-min __v7 __v8)) ()))
+(function __v () Math :no-merge :unextractable :internal-let)
+(set (__v) (Add 1 2))
+(set (__AddView 1 2) (__v))
+(set (__UF_Math (ordering-max (__v) (__v)) (ordering-min (__v) (__v))) ())
+(run-schedule (seq (saturate (seq (run __rebuilding_cleanup) (saturate (run __parent)) (saturate (run __uf_function_index)) (run __rebuilding))) (run __delete_subsume_ruleset)))
+(rule ((= __v1 (__AddView a b)))
+      ((let __v3 (Add a b))
+       (set (__AddView a b) __v3)
+       (set (__UF_Math (ordering-max __v3 __v3) (ordering-min __v3 __v3)) ())
+       (let __v4 (Add b a))
+       (set (__AddView b a) __v4)
+       (set (__UF_Math (ordering-max __v4 __v4) (ordering-min __v4 __v4)) ())
+       (set (__UF_Math (ordering-max __v3 __v4) (ordering-min __v3 __v4)) ()))
          :name "commutativity")
-(check (= __v10 (__AddView 1 2 __v9))
-(= __v12 (__AddView 2 1 __v11))
-(= __v9 __v11))
-(run-schedule (seq (saturate (seq (run __rebuilding_cleanup) (saturate (run __single_parent)) (saturate (run __parent)) (saturate (run __uf_function_index)) (run __rebuilding))) (run __delete_subsume_ruleset)))
+(check (= __v5 (__AddView 1 2))
+(= __v6 (__AddView 2 1))
+(= __v5 __v6))
+(run-schedule (seq (saturate (seq (run __rebuilding_cleanup) (saturate (run __parent)) (saturate (run __uf_function_index)) (run __rebuilding))) (run __delete_subsume_ruleset)))
diff --git a/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function2.snap b/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function2.snap
index 5a58d4475..f9d9b3eb3 100644
--- a/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function2.snap
+++ b/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function2.snap
@@ -3,41 +3,24 @@ source: src/proofs/proof_tests.rs
 expression: snapshot
 ---
 (ruleset __parent)
-(ruleset __single_parent)
 (ruleset __uf_function_index)
 (ruleset __rebuilding)
 (ruleset __rebuilding_cleanup)
 (ruleset __delete_subsume_ruleset)
 (sort __view)
 (constructor add (i64 i64 i64) __view :unextractable :internal-hidden)
-(function __addView (i64 i64 i64) Unit :merge old :unextractable :internal-term-constructor add)
+(function __addView (i64 i64) i64 :merge old :unextractable :internal-term-constructor add :identity-values 1)
 (constructor __to_delete_add (i64 i64) __view :internal-hidden)
 (constructor __to_subsume_add (i64 i64) __view :internal-hidden)
-(sort __mergecleanupsort)
-(constructor __mergecleanup (i64 i64) __mergecleanupsort :internal-hidden)
-(rule ((__addView c0_ c1_ old)
-       (__addView c0_ c1_ new)
-       (!= old new)
-       (= (ordering-max old new) new))
-      ((set (__addView c0_ c1_ old) ())
-       (__mergecleanup old old)
-       (__mergecleanup old new))
-        :ruleset __rebuilding :name "__merge_rule")
-(rule ((__mergecleanup merged old)
-       (__addView c0_ c1_ merged)
-       (__addView c0_ c1_ old)
-       (!= merged old))
-      ((delete (__addView c0_ c1_ old)))
-        :ruleset __rebuilding_cleanup :name "__merge_cleanup")
 (rule ((__to_delete_add c0_ c1_)
-       (__addView c0_ c1_ out))
-      ((delete (__addView c0_ c1_ out))
+       (= out (__addView c0_ c1_)))
+      ((delete (__addView c0_ c1_))
        (delete (__to_delete_add c0_ c1_)))
         :ruleset __delete_subsume_ruleset :name "__delete_rule")
 (rule ((__to_subsume_add c0_ c1_)
-       (__addView c0_ c1_ out))
-      ((subsume (__addView c0_ c1_ out)))
+       (= out (__addView c0_ c1_)))
+      ((subsume (__addView c0_ c1_)))
         :ruleset __delete_subsume_ruleset :name "__delete_rule_subsume")
-(check (= __v (__addView 0 0 __n))
+(check (= __n (__addView 0 0))
 (= __n 0))
-(run-schedule (seq (saturate (seq (run __rebuilding_cleanup) (saturate (run __single_parent)) (saturate (run __parent)) (saturate (run __uf_function_index)) (run __rebuilding))) (run __delete_subsume_ruleset)))
+(run-schedule (seq (saturate (seq (run __rebuilding_cleanup) (saturate (run __parent)) (saturate (run __uf_function_index)) (run __rebuilding))) (run __delete_subsume_ruleset)))
diff --git a/src/scheduler.rs b/src/scheduler.rs
index eb5436fc1..154099b1f 100644
--- a/src/scheduler.rs
+++ b/src/scheduler.rs
@@ -338,6 +338,8 @@ impl SchedulerRuleInfo {
             .collect();
         let decided = egraph.backend.add_table(FunctionConfig {
             schema,
+            num_values: 1,
+            identity_values: None,
             default: DefaultVal::Const(unit),
             merge: MergeFn::AssertEq,
             name: "backend".to_string(),
diff --git a/src/serialize.rs b/src/serialize.rs
index 83ab82920..ef0edebb5 100644
--- a/src/serialize.rs
+++ b/src/serialize.rs
@@ -131,6 +131,7 @@ impl EGraph {
             &Function,
             Vec<Value>, // inputs
             Value,      // output
+            ArcSort,    // output sort (pair-first component for pair views)
             bool,       // is subsumed
             egraph_serialize::ClassId,
             egraph_serialize::NodeId,
@@ -148,8 +149,22 @@ impl EGraph {
                     truncated_functions.push(name.clone());
                     return false;
                 }
-                let (out, inps) = row.vals.split_last().unwrap();
-                let class_id = self.value_to_class_id(&function.schema.output, *out);
+                // For a pair-valued function (two value columns) the real
+                // output (eclass) is the first value column; the proof rides in
+                // the second. Serialize using the first value column and its
+                // component sort.
+                let (out, inps, out_sort) = if let Some((first, _second)) =
+                    EGraph::pair_components(&function.schema.output)
+                {
+                    let n = row.vals.len();
+                    let out = &row.vals[n - 2];
+                    let inps = &row.vals[..n - 2];
+                    (out, inps, first)
+                } else {
+                    let (out, inps) = row.vals.split_last().unwrap();
+                    (out, inps, function.schema.output.clone())
+                };
+                let class_id = self.value_to_class_id(&out_sort, *out);
                 if function.decl.internal_let {
                     let_bindings
                         .entry(class_id.clone())
@@ -160,6 +175,7 @@ impl EGraph {
                         function,
                         inps.to_vec(),
                         *out,
+                        out_sort.clone(),
                         row.subsumed,
                         class_id,
                         self.to_node_id(
@@ -185,8 +201,8 @@ impl EGraph {
         // amoung all possible options.
         let node_ids: NodeIDs = all_calls.iter().fold(
             HashMap::default(),
-            |mut acc, (func, _input, _output, _subsumed, class_id, node_id)| {
-                if func.schema.output.is_eq_sort() {
+            |mut acc, (_func, _input, _output, out_sort, _subsumed, class_id, node_id)| {
+                if out_sort.is_eq_sort() {
                     acc.entry(class_id.clone())
                         .or_default()
                         .push_back(node_id.clone());
@@ -201,8 +217,8 @@ impl EGraph {
             let_bindings,
         };
 
-        for (func, input, output, subsumed, class_id, node_id) in all_calls {
-            self.serialize_value(&mut serializer, &func.schema.output, output, &class_id);
+        for (func, input, output, out_sort, subsumed, class_id, node_id) in all_calls {
+            self.serialize_value(&mut serializer, &out_sort, output, &class_id);
 
             assert_eq!(input.len(), func.schema.input.len());
             let children: Vec<_> = input
diff --git a/src/typechecking.rs b/src/typechecking.rs
index 53cf2b405..bcdb09738 100644
--- a/src/typechecking.rs
+++ b/src/typechecking.rs
@@ -734,13 +734,9 @@ impl TypeInfo {
                 fdecl.span.clone(),
             ));
         }
-        // View tables (with term_constructor) must have at least one input (the e-class)
-        if fdecl.term_constructor.is_some() && fdecl.schema.input.is_empty() {
-            return Err(TypeError::TermConstructorNoInputs(
-                fdecl.name.clone(),
-                fdecl.span.clone(),
-            ));
-        }
+        // Note: FD view tables (with term_constructor) may have zero inputs
+        // (e.g. the view for a global), because the e-class now lives in the
+        // value column rather than as the last input.
         let ftype = self.function_to_functype(fdecl)?;
         if self.func_types.insert(fdecl.name.clone(), ftype).is_some() {
             return Err(TypeError::FunctionAlreadyBound(
@@ -759,29 +755,51 @@ impl TypeInfo {
         bound_vars.insert("old", (fdecl.span.clone(), output_type.clone()));
         bound_vars.insert("new", (fdecl.span.clone(), output_type.clone()));
 
+        // A merge runs as an action-side write and must be a pure write (use
+        // old/new, call primitives, or mint constructor terms): live DB reads
+        // would be untracked by seminaive execution, so reading a non-constructor
+        // function in a merge is disallowed in all modes.
+        let merge = match &fdecl.merge {
+            Some(merge) => Some(self.typecheck_standalone_expr(
+                symbol_gen,
+                merge,
+                &bound_vars,
+                Context::Write,
+            )?),
+            None => None,
+        };
+        // Effect actions of a block-form merge: resolved + typechecked via
+        // the same pipeline as rule actions, with `old`/`new` bound.
+        let merge_action = self.typecheck_standalone_actions(
+            symbol_gen,
+            &fdecl.merge_action,
+            &bound_vars,
+            Context::Write,
+        )?;
+
+        // Reject reading a non-constructor function in the merge value or any
+        // block-form action. Flags only `Func` with `subtype == Custom &&
+        // !is_global`, so constructor-, primitive-, and trivial-bodied merges
+        // are not flagged.
+        if let Some(merge) = &merge {
+            self.check_merge_lookup_expr(merge)?;
+        }
+        self.check_no_function_lookups_in_merge_actions(&merge_action)?;
+
         Ok(ResolvedFunctionDecl {
             name: fdecl.name.clone(),
             subtype: fdecl.subtype,
             schema: fdecl.schema.clone(),
             resolved_schema: ResolvedCall::Func(self.func_types.get(&fdecl.name).unwrap().clone()),
-            merge: match &fdecl.merge {
-                // Merge expressions run as part of action-side table updates:
-                // writes are allowed, but live DB reads would be untracked by
-                // seminaive rule execution.
-                Some(merge) => Some(self.typecheck_standalone_expr(
-                    symbol_gen,
-                    merge,
-                    &bound_vars,
-                    Context::Write,
-                )?),
-                None => None,
-            },
+            merge,
+            merge_action,
             cost: fdecl.cost,
             unextractable: fdecl.unextractable,
             internal_hidden: fdecl.internal_hidden,
             internal_let: fdecl.internal_let,
             span: fdecl.span.clone(),
             term_constructor: fdecl.term_constructor.clone(),
+            identity_values: fdecl.identity_values,
         })
     }
 
@@ -915,6 +933,42 @@ impl TypeInfo {
         Ok(())
     }
 
+    fn check_merge_lookup_expr(&self, expr: &ResolvedExpr) -> Result<(), TypeError> {
+        if let Some((name, span)) = self.expr_function_lookup(expr) {
+            return Err(TypeError::LookupInMergeDisallowed(name, span));
+        }
+        Ok(())
+    }
+
+    fn check_no_function_lookups_in_merge_actions(
+        &self,
+        actions: &ResolvedActions,
+    ) -> Result<(), TypeError> {
+        for action in actions.iter() {
+            match action {
+                GenericAction::Let(_, _, rhs) => self.check_merge_lookup_expr(rhs)?,
+                GenericAction::Set(_, _, args, rhs) => {
+                    for arg in args.iter() {
+                        self.check_merge_lookup_expr(arg)?;
+                    }
+                    self.check_merge_lookup_expr(rhs)?;
+                }
+                GenericAction::Union(_, lhs, rhs) => {
+                    self.check_merge_lookup_expr(lhs)?;
+                    self.check_merge_lookup_expr(rhs)?;
+                }
+                GenericAction::Change(_, _, _, args) => {
+                    for arg in args.iter() {
+                        self.check_merge_lookup_expr(arg)?;
+                    }
+                }
+                GenericAction::Panic(..) => {}
+                GenericAction::Expr(_, expr) => self.check_merge_lookup_expr(expr)?,
+            }
+        }
+        Ok(())
+    }
+
     fn check_no_function_lookups_in_actions(
         &self,
         actions: &ResolvedActions,
@@ -1118,6 +1172,12 @@ impl TypeInfo {
     /// Global function calls are allowed since they get desugared to constructors.
     /// Returns Some(span) if a lookup is found, None otherwise.
     pub fn expr_has_function_lookup(&self, expr: &ResolvedExpr) -> Option<Span> {
+        self.expr_function_lookup(expr).map(|(_, span)| span)
+    }
+
+    /// Like [`Self::expr_has_function_lookup`], but also returns the name of the
+    /// offending non-constructor function (for error messages).
+    fn expr_function_lookup(&self, expr: &ResolvedExpr) -> Option<(String, Span)> {
         use ast::GenericExpr;
 
         expr.find(&mut |e| {
@@ -1125,7 +1185,7 @@ impl TypeInfo {
                 && func_type.subtype == FunctionSubtype::Custom
                 && !self.is_global(&func_type.name)
             {
-                return Some(span.clone());
+                return Some((func_type.name.to_string(), span.clone()));
             }
             None
         })
@@ -1175,6 +1235,10 @@ pub enum TypeError {
     ConstructorOutputNotSort(String, Span),
     #[error("{1}\nValue lookup of non-constructor function {0} in rule is disallowed.")]
     LookupInRuleDisallowed(String, Span),
+    #[error(
+        "{1}\nValue lookup of non-constructor function {0} in a merge is disallowed; a merge must be a pure write (it may use old/new, call primitives, or build constructors, but not read another function)."
+    )]
+    LookupInMergeDisallowed(String, Span),
     #[error("{1}\nCannot set constructor {0}. Use `union` instead or declare {0} as a function.")]
     SetConstructorDisallowed(String, Span),
     #[error("All alternative definitions considered failed\n{}", .0.iter().map(|e| format!("  {e}\n")).collect::<Vec<_>>().join(""))]
diff --git a/tests/fail-typecheck/merge_reads_function.egg b/tests/fail-typecheck/merge_reads_function.egg
new file mode 100644
index 000000000..172c2ad38
--- /dev/null
+++ b/tests/fail-typecheck/merge_reads_function.egg
@@ -0,0 +1,10 @@
+; A `:merge` body must be a pure write, so reading another
+; (non-constructor) function in it is a live-DB read that
+; seminaive execution can't track. It is rejected at
+; typecheck in all modes (LookupInMergeDisallowed).
+;
+; Reading `foo` in `bar`'s merge below is such a read.
+
+(function foo () i64 :no-merge)
+
+(function bar () i64 :merge (foo))
diff --git a/tests/merge-eq-sort-trivial.egg b/tests/merge-eq-sort-trivial.egg
new file mode 100644
index 000000000..064ad4f03
--- /dev/null
+++ b/tests/merge-eq-sort-trivial.egg
@@ -0,0 +1,24 @@
+;; Trivial eq-sort-output custom merges (`:merge old` / `:merge new`):
+;; value-replacement merges over an eq-sort output that route onto the FD
+;; pair-valued view (no union, no congruence). No action lookups, so the file
+;; supports proofs and runs in every treatment.
+
+(datatype T (A) (B))
+
+;; `:merge old`: on a key collision keep the first value set.
+(function keep-old (i64) T :merge old)
+;; `:merge new`: on a key collision keep the last value set.
+(function keep-new (i64) T :merge new)
+
+;; Collide on the same key (0) with two different eq-sort values A and B.
+(set (keep-old 0) (A))
+(set (keep-old 0) (B))
+
+(set (keep-new 0) (A))
+(set (keep-new 0) (B))
+
+(run 1)
+
+;; keep-old kept the first value (A); keep-new kept the last value (B).
+(check (= (keep-old 0) (A)))
+(check (= (keep-new 0) (B)))
diff --git a/tests/merge_read.egg b/tests/merge_read.egg
deleted file mode 100644
index 09cbb5402..000000000
--- a/tests/merge_read.egg
+++ /dev/null
@@ -1,7 +0,0 @@
-(function foo () i64 :no-merge)
-
-(function bar () i64 :merge (foo))
-
-(set (bar) 0)
-
-(fail (set (bar) 1))
\ No newline at end of file
diff --git a/tests/naive-action-lookup.egg b/tests/naive-action-lookup.egg
index 5676e435b..40dd172e8 100644
--- a/tests/naive-action-lookup.egg
+++ b/tests/naive-action-lookup.egg
@@ -1,9 +1,7 @@
 ; `:naive` widens a rule's contexts to Read/Full and skips the "no function
-; lookups in actions" check, so the RHS may read the database — including
-; function-table lookups. Unlike `:unsafe-seminaive` it re-matches the whole
-; database every iteration, so the read is safe. Function lookups in actions
-; aren't representable in the term/proof encoding, so this only runs on the
-; default backend.
+; lookups in actions" check, so the RHS may read the database. It re-matches the
+; whole database each iteration, so the read is safe. Action lookups aren't
+; representable in the term/proof encoding, so this only runs on the default backend.
 
 (function f (i64) i64 :merge (max old new))
 (set (f 1) 100)
diff --git a/tests/snapshots/files__fail-typecheck__merge_reads_function.snap b/tests/snapshots/files__fail-typecheck__merge_reads_function.snap
new file mode 100644
index 000000000..8291c2301
--- /dev/null
+++ b/tests/snapshots/files__fail-typecheck__merge_reads_function.snap
@@ -0,0 +1,6 @@
+---
+source: tests/files.rs
+expression: err_msg
+---
+In 10:29-33 of merge_reads_function.egg: (foo)
+Value lookup of non-constructor function foo in a merge is disallowed; a merge must be a pure write (it may use old/new, call primitives, or build constructors, but not read another function).
diff --git a/tests/snapshots/files__proof_unsupported_files.snap b/tests/snapshots/files__proof_unsupported_files.snap
index 190f0450a..0f8498bcc 100644
--- a/tests/snapshots/files__proof_unsupported_files.snap
+++ b/tests/snapshots/files__proof_unsupported_files.snap
@@ -35,7 +35,6 @@ looking_up_nonconstructor_in_rewrite_good.egg
 luminal-llama.egg
 map.egg
 math.egg
-merge_read.egg
 multiset.egg
 naive-action-lookup.egg
 nested-container-dirty-propagation.egg
diff --git a/tests/snapshots/files__shared_snapshot_merge_read.snap b/tests/snapshots/files__shared_snapshot_merge_eq_sort_trivial.snap
similarity index 64%
rename from tests/snapshots/files__shared_snapshot_merge_read.snap
rename to tests/snapshots/files__shared_snapshot_merge_eq_sort_trivial.snap
index 139053a0c..78237bacc 100644
--- a/tests/snapshots/files__shared_snapshot_merge_read.snap
+++ b/tests/snapshots/files__shared_snapshot_merge_eq_sort_trivial.snap
@@ -2,5 +2,7 @@
 source: tests/files.rs
 expression: snapshot_content_across_treatments
 ---
-((bar 1)
- (foo 0))
+((A 1)
+ (B 1)
+ (keep-new 1)
+ (keep-old 1))
diff --git a/tests/unsafe-seminaive-read-prim.egg b/tests/unsafe-seminaive-read-prim.egg
index 1999bce1f..18dabcbf0 100644
--- a/tests/unsafe-seminaive-read-prim.egg
+++ b/tests/unsafe-seminaive-read-prim.egg
@@ -1,10 +1,7 @@
-; `:unsafe-seminaive` also widens a rule's primitive contexts to
-; Read/Full, so the RHS can call primitives that read the database — not
-; just function-table lookups. `unstable-multiset-fill-index` is a
-; FullPrim (it reads a multiset and writes an index function), which the
-; default seminaive action context (Write) does not admit — without
-; `:unsafe-seminaive` the call doesn't even resolve. With it, the rule
-; keeps delta evaluation but the FullPrim is available in the RHS.
+; `:unsafe-seminaive` also widens a rule's primitive contexts to Read/Full, so
+; the RHS can call database-reading primitives. `unstable-multiset-fill-index`
+; is a FullPrim that the default seminaive action context (Write) doesn't admit;
+; without `:unsafe-seminaive` it wouldn't even resolve.
 
 (datatype Math (Num i64))
 (sort Maths (MultiSet Math))
diff --git a/tests/unsafe-seminaive.egg b/tests/unsafe-seminaive.egg
index 6ee745a9e..cfda46e2b 100644
--- a/tests/unsafe-seminaive.egg
+++ b/tests/unsafe-seminaive.egg
@@ -1,12 +1,9 @@
-; The `:unsafe-seminaive` rule option keeps seminaive (delta) evaluation
-; but compiles the rule with the permissive Read/Full primitive contexts
-; and skips the "no function lookups in actions" typecheck — so the RHS
-; can perform arbitrary database reads, including function-table lookups.
-;
-; It is unsafe: a read on a seminaive RHS observes the database
-; mid-iteration, so results can depend on evaluation order. It's also a
-; direct-backend feature — the term/proof encoding rejects it, so this
-; file only runs on the default backend.
+; `:unsafe-seminaive` keeps seminaive (delta) evaluation but compiles the rule
+; with the permissive Read/Full contexts and skips the "no function lookups in
+; actions" typecheck, so the RHS can read the database. It is unsafe because a
+; read on a seminaive RHS observes the database mid-iteration (results can depend
+; on order). The term/proof encoding rejects it, so this only runs on the default
+; backend.
 
 (function f (i64) i64 :merge (max old new))
 (set (f 1) 100)