Spanning tree of a connected finite multigraph

Let $V$ and $E$ be finite types with decidable equality, and let $\mathrm{hd}, \mathrm{tl} \colon E \to V$ be two maps, to be read as the head and tail of each edge of a directed multigraph with vertex set $V$ and edge set $E$. For a function $c \colon E \to \mathbb{Z}$, regarded as an integral $1$-chain, write its boundary at a vertex $w$ as $\sum_{\mathrm{hd}(e) = w} c(e) - \sum_{\mathrm{tl}(e) = w} c(e)$. The hypothesis is that for every ordered pair of vertices $u, v$ there exists $c \colon E \to \mathbb{Z}$ whose boundary at each $w$ equals $[w = v] - [w = u]$, the difference of the two indicator values. The conclusion asserts the existence of a finite set $T$ of edges, a subset of $E$, such that for every ordered pair $u, v$ of vertices there is exactly one $c \colon E \to \mathbb{Z}$ which vanishes at every edge outside $T$ and whose boundary at each $w$ equals $[w = v] - [w = u]$. Thus existence of chains with prescribed boundary $v - u$ for all pairs is upgraded to existence and uniqueness of such chains supported on a fixed edge set $T$.

This is the existence of a spanning tree of a finite connected multigraph, phrased homologically: connectivity is expressed by solvability of the boundary equation $\partial c = v - u$, and the spanning-tree property of $T$ by unique solvability among chains supported on $T$ (existence for all pairs says $T$ spans, uniqueness says $T$ carries no nonzero cycle). It feeds the construction of fundamental cycles and the computation of the first homology of the graphs arising in the Čerednik–Drinfeld setting, being cited by CerednikDrinfeld.Omega.exists_isUnit_det_pathCycle_and_span_pathCycle.