Quantifier-free induction for lists

We investigate quantifier-free induction for Lisp-like lists constructed inductively from the empty list \( nil \) $\mathit{nil}$ and the operation \({\textit{cons}}\) $\mathit{cons}$ , that adds an element to the front of a list. First we show that, for \(m \ge 1\) $m\ge 1$ , quantifier-free \(m\) $m$ -step induction does not simulate quantifier-free \((m + 1)\) $(m+1)$ -step induction. Secondly, we show that for all \(m \ge 1\) $m\ge 1$ , quantifier-free \(m\) $m$ -step induction does not prove the right cancellation property of the concatenation operation on lists defined by left-recursion.