Is there a proof of the recursive algorithm for generating all permutations of a sequence?
Hint: Prove by induction that $\mathrm{permute}(l,n)$:


Adds to $P$ all permutations obtained from $l$ by permuting coordinates $n,\ldots,|l|$.
Leaves $l$ unchanged. That is, the value of $l$ after running the function is the same as its value before running it.