# On permutations

Define the following relationships on `(list A)`:
- The list
*l'* is obtained from *l* by transposing two consecutive
items.
- The list
*l'* is obtained from *l* by a finite number of such transpositions. * We say that **l'* is a permutation of *l*.

*
Show that the second one is an equivalence relation.
*## Solution

Look at this file
### Note

You could also define the relationship `perm` as
`(Rstar _ transpose)`. In this case, you first have
to load the module `Rstar` of the library `Relations`,
and prove that the reflexive transitive closure of a symmetric relation
is symmetric too.

Follow this link

Going home

Pierre Castéran