Kirigami node remapping happens "too late" to properly remap some expressions

[alberdingk-thijm]

Per commit 89efe79, we currently have a bug in Kirigami when handling remapping of node expressions. examples/kirigami/node-eq.nv gives a MWE of this.
Essentially, the issue is as follows:
When encoding a fold over assertions of the form assert foldNodes (fun u v acc -> acc && assertNode u v) sol true, we start by unrolling sol and flattening tuples to obtain a statement that reasons over each node:

assert true && (assertNode 0n sol-proj-0 sol-proj-1 ...) && (assertNode 1n sol-proj-k sol-proj-k) && ...

where each assertNode has k arguments where k is the number of arguments used to encode the attribute for that particular node.
This leads to an issue when assertNode reasons over expressions that contain references to these nodes.
For instance, the expression

let assertNode u v = if u = 1n then true else v = 0

will have the value of u populated to now leave us with:

assert true && (if 0n = 1n then true else sol-proj-0 = 0) && (if 1n = 1n then true else sol-proj-k = 0) && ...

Suppose we have two nodes, 0n and 1n, which are placed in separate partitions: then we remap 1n to 0n in partition 1, and we want to eliminate additional conjuncts, leaving us with:

(* Partition 0 *)
assert (if 0n = 1n then true else sol-proj-0 = 0) (* ==> assert (if false then true else sol-proj-0 = 0) *)
(* Partition 1 *)
assert (if 0n = 1n then true else sol-proj-0 = 0) (* ==> assert (if true then true else sol-proj-0 = 0) *)

The problem here is that our current approach doesn't know to handle 0n = 1n differently in partition 1, since we'd need to remap 1n to 0n, but since we have that 0n has been cut, we don't recognize that the LHS of the equality should be kept and so both partitions reduce this expression to false.
The best way to handle this may be if we transformed assertNode from the top, we could end up with

(* Partition 0 *)
let assertNode u v = if false then true else v = 0
(* Partition 1 *)
let assertNode u v = if u = 0n then true else v = 0

which would then work once map unrolling is performed.