Notation in this question derives from Haskell as follows. Let $[A]$ denote the collection of lists whose elements are drawn from the set $A$, so e.g. $[\mathbb{Z}]$ is the set of integer lists. Denote the empty list of any type by $[]$. Denote a single-element list by by $[a]$. We may write any nonempty list as a:x, where $a \in A$ is the first element and $x \in [A]$ is the (possibly empty) tail of the list. Denote list concatenation by a ++ b. Lists are finite and allow repetitions: 1 : [1] is a valid list, which has two elements ($1$ and $1$).
The Haskell code is:
perm :: [Int] -> [[Int]]
perm z = f([], [], z) where
f(x, y, []) = []
f(x, [], [a]) = [x ++ [a]]
f(x, y, a:z) = f(x ++ [a], [], y ++ z) ++ f(x, y ++ [a], z)
How do I prove that the function returns a permutation by using structural induction?
This is more of an expository hint than anything; I'm answering the "how" rather than giving an answer to the exercise.
You need to find an appropriate wellfounded partial order on $[\mathbb{Z}] \times [\mathbb{Z}] \times [\mathbb{Z}]$, such that the following relations hold for all lists $x, y, z \in [\mathbb{Z}]$ and for all $a \in \mathbb{Z}$:
In fact, the actual elements of the list are unimportant; your definition is completely generic on the type $\mathbb{Z}$. So we should be able to answer this question by only considering the lengths of the lists. In fact, an equivalent formulation of your question is: prove by induction that $g : \mathbb{N}^3 \to \mathbb{N}$ is well-defined, where $g$ is given by
(Moreover, you actually also want $g(0, 0, c) = c!$, but that's a story for another time.)
The way to do this is to find a function $i : \mathbb{N}^3 \to \mathbb{N}$ such that $i(a+1, 0, b+c) < i(a, b, c+1)$ (so that the first recursive call can be assumed inductively to terminate) and such that $i(a, b+1, c) < i(a, b, c+1)$ (so that the second recursive call can be assumed inductively to terminate). Once you've done this, you're done by induction on the value of $i$.