Equivalence between two definitions of permutations of lists

There are (at least) two ways of defining permutations between lists: Show that both definitions are logically equivalent.
Use this equivalence to prove easily the following fact:
Lemma counterexample : ~ permI (2::3::5::5::8::7::4::nil) 


This file
Look also at the following exercises on permutations : this one and this one .
Going home
Exercise proposed by Houda Anoun