fix a line to work with older Agda, and some commented out experiment (in Permutations)
merge and move proof forward