Defining a predicate on the structure of a string
No, in the recursive case you need to take the first symbol out of $t$, so you need at that point to unfold the structure of $t$.

Note that, as in functional programming, the functions $head$ and $tail$ should be used with great care since they are not total: $head(\epsilon)$ and $tail(\epsilon)$ are undefined. Hence, remember to require $t\neq\epsilon$ every time you use $head(t)$ or $tail(t)$, and to handle the $\epsilon$ case elsewhere.

I would tend to use your first solution, which needs a similar fix.

$$
\begin{array}{l}
{\sf pre}(\epsilon,t):= \sf true \\
{\sf pre}(\alpha.s,\epsilon):=\sf false \\
{\sf pre}(\alpha.s,\beta.t):=(\alpha=\beta)\land {\sf pre}(s,t)
\end{array}
$$

In this way you are not assuming that the second argument is non empty. You are still assuming that it is a word, but that's needed.