Yes! Here is a proof which is slightly different from both your proof and the proof in Mines–Richman–Ruitenberg.

First define the similarity relation on $\mathrm{List}(R \times X)$ as in Mines–Richman–Ruitenberg as the smallest equivalence relation generated by their clauses (i), (ii) and (iii). I'd argue that this is the obvious thing to do if you set out to construct the free module.

We'll then show: Lists $[\langle a_1, x_1\rangle, \ldots, \langle a_n, x_n \rangle]$ and $[\langle b_1, y_1\rangle, \ldots, \langle b_m, y_m \rangle]$ are similar if and only if for all $x \in X$, $I \subseteq \{1,\ldots,n\}$, $J \subseteq \{1,\ldots,m\}$ (I just mean the detachable subsets here) such that $x_i = x$ for all $i \in I$ and $y_j = x$ for all $j \in J$, there are supersets $I' \supseteq I$ and $J' \supseteq J$ (again, $I'$ and $J'$ should be detachable) such that $x_i = x$ for all $i \in I'$, $y_j = x$ for all $j \in J'$ and $\sum_{i \in I'} a_i = \sum_{j \in J'} b_j$.

This is done in three steps:

- The proposed characterization of similarity defines an equivalence relation (transitivity is slightly nontrivial, as in your proof).
- That equivalence relation encompasses similarity.
- It is the smallest equivalence relation satisfying (i), (ii) and (iii). For this step to work, it's important that the additive group of the ring is (as all groups are) cancellative. That is, this step wouldn't generalize to rigs $(R,0,1,+,\cdot)$ where $(R,0,+)$ is just required to be a commutative monoid.

With the characterization of similarity in hand, the injectivity of the unit is then easy to establish: Assume that the lists $[\langle 1, x_1\rangle]$ and $[\langle 1, y_1\rangle]$ are similar. By the characterization (applied to $x_1$, $I = \{1\}$, $J = \emptyset$), there is a detachable set $J' \subseteq \{1\}$ such that $y_j = x_1$ for all $j \in J'$ and $1 = \sum_{j \in J'} 1$. We have $1 \in J'$ or $1 \not\in J'$. If $1 \not\in J'$, then $1 = 0$ in $R$; a contradiction. Thus $1 \in J'$. So $y_1 = x_1$.

**Edit.** Here are details on step 3. Let $({\approx})$ be the equivalance relation given by the proposed characterization. Let $({\sim})$ be an equivalence relation on $\mathrm{List}(R \times X)$ which satisfies clauses (i), (ii) and (iii). We verify $v \approx w \Rightarrow v \sim w$ by induction on the combined length of $v$ and $w$. The base case ($v = w = [] = \text{empty list}$) is immediate.

Now let lists $v$ and $w$ be given such that $v \approx w$ and such that at least one of the lists, let's say $v$, has positive length. Write $v = [\langle a_1,x_1\rangle, \ldots, \langle a_n,x_n \rangle]$ and $w = [\langle b_1,y_1\rangle, \ldots, \langle b_m,x_m \rangle]$. The definition of $v \approx w$ (applied to $x = x_1$, $I = \{1\}$, $J = \emptyset$) yields index sets $I'$ and $J'$ such that $x_i = x_1$ for all $i \in I'$, $y_j = x_1$ for all $j \in J'$, $c := \sum_{i \in I'} a_i = \sum_{j \in J'} b_j$. Let $\hat v$ and $\hat w$ be obtained from $v$ and $w$ by removing all those entries whose index is an element of $I'$ respectively $J'$. We claim:

(a) $\hat v \approx \hat w$

(b) $v \sim w$

Claim (b) follows from claim (a): If $\hat v \approx \hat w$, then by induction also $\hat v \sim \hat w$. Then also $(\langle c,x_1\rangle :: \hat v) \sim (\langle c,x_1\rangle :: \hat w)$ (where $({::})$ is adding an element in front). Since $({\sim})$ satisfies (i), (ii) and (iii), $v \sim w$.

On to claim (a). Let $x \in X$. Let $\hat I$ and $\hat J$ be (detachable) sets of indices of entries of $\hat v$ respectively $\hat w$ such that the corresponding entries mention $x$. These index sets can also be seen as subsets of $\{1,\ldots,n\}$ respectively $\{1,\ldots,m\}$, by slightly juggling the indices. Therefore the definition of $v \approx w$ yields index sets $I''$ and $J''$. It might be the case that $I''$ and $J''$ contain only indices which can be reinterpreted to be indices in $\hat v$ respectively $\hat w$. In this case we are done.

But it could also happen that $I''$ has nontrivial overlap with $I'$ or that $J''$ has nontrivial overlap with $J'$. In this case $I''$ and $J''$ are of no further use, but we learned that $x = x_1$. We now apply the definition of $v \approx w$ again, this time to $x_1$, $\hat I \cup I'$ and $\hat J \cup J'$ (where we first juggle the indices in $\hat I$ and $\hat J$ accordingly before taking the union). This gives us index sets $I'''$ and $J'''$. We have $\sum_{i \in I'''} a_i = \sum_{j \in J'''} b_j$. By cancellativity, also $\sum_{i \in I''''} a_i = \sum_{j \in J''''} b_j$ where $I'''' = I''' \setminus I'$ and $J'''' = J''' \setminus J'$. Hence we're done.

Bijective matrix algebra, Linear Algebra and its Applications, Volume 416, Issues 2--3, 15 July 2006, pp. 917--944 also seems of relevance -- though the waytheyhave built it up, it probably requires all the sets to have decidable equality. $\endgroup$ – darij grinberg Jun 11 '18 at 19:59