added counterexample to Permutation.agda