I have a claim that I believe to be true, but am not sure how to prove it.
Suppose I have a (strict) partially ordered set $(A, <)$ and some other set $B$ and a function $f : A \times B \to B$ such that the following holds for all $b \in B$ and $a, a' \in A$ (with $a \neq a'$):
$$\neg(a < a') \land \neg (a' < a) \implies f(a, f(a', b)) = f(a', f(a, b)).$$
In other words, $f(-, b)$ "commutes" with the incomparable elements in $A$ for any $b \in B$.
Then I believe the following is true:
Notation: $\langle \rangle$ is the empty list and $a \cdot l$ prepends the list $l$ with element $a$.
Let $A^{*}$ be lists of elements of $A$. Define $f^{*} : A^{*} \times B \to B$ inductively by $f^{*}(\langle \rangle, b) = b$ and $f^{*}(a \cdot l, b) = f^{*}(l, f(a, b))$. Suppose $l, l' \in A^{*}$ are lists which (1.) contain the same elements and (2.) both "refine" $<$, i.e. $l$ is the same as $l'$ up to permutations of incomparable elements. Said another way, the list order is consistent with $<$. Then: $f^{*}(l, b) = f^{*}(l', b)$.
For example, if $y < x$ and $y < z$, and $x, z$ are incomparable, then these two lists both refine $<$: $l = \langle y, x, z \rangle$ and $l’= \langle y, z, x \rangle$. It’s clear that $f^*(l, b) = f^*(l’,b)$.
Intuition: the incomparable elements of $l'$ may be "permuted" to make the effect of $f^{*}$ on $l'$ "the same" as the effect of $f^{*}$ on $l$. I don't think a standard induction on the list length will work here, but I am not sure what technique the formal proof would involve. It seems like the kind of thing that order theory would have resolved at some point, but I haven't seen this anywhere.