Multivariate big-step induction conjecture for right cancellation of list concatenation

Let $T_{1}$ be the base theory for list concatenation. For a finite sequence of pairwise distinct list variables $\vec{X}=(X_{1},\dots,X_{m})$ and a sequence of non-zero natural numbers $\vec{p}=(p_{1},\dots,p_{m})$, let $I^{\mathsf{list}}_{\vec{X}\curvearrowright\vec{p}}\varphi$ be the corresponding multivariate big-step list-induction axiom, and let $\mathrm{Open}(\mathcal{L}_{1})\text{-}\mathrm{IND}^{\mathsf{list}}_{\nearrow_{\curvearrowright}}$ be the theory generated by these axioms for open formulas. For lists $X,Y,Z$, write $Y\frown X$ for concatenation. Right-cancellation conjecture.

$$T_{1} + {\mathrm{Open}(\mathcal{L}_{1})}\text{-}\mathrm{IND}^{\mathsf{list}}_{\nearrow_{\curvearrowright}} \not\vdash Y \frown X = Z \frown X \rightarrow Y = Z.$$

The claim concerns whether multivariate heterogeneous big-step induction can prove right cancellation, a simple and practically relevant property of finite lists. The source presents the claim after defining the induction schema; its resolution is not supplied and remains open.