Let $t,a$ are some terms in a first-order language, $x$ is a free variable, the notation $t[x:=a]$ denotes the rezult of replacement in $t$ every occurrence of $x$ with $a$.
Suppose, we have a term equation $Z[x:=a] = t$, where $Z$ is a term variable. If $a$ is a free variable, $t$ does not contain $x$, then a solution is $Z = t[a:=x]$ because $Z[x:=a] = t[a:=x][x:=a] = t$.
In which other cases can we solve this equation?
