Inductive permI :list A ->list A ->Prop:=
|permI_refl:forall l, permI l l
|permI_cons:forall a l0 l1, permI l0 l1-> permI (a::l0)(a::l1)
|permI_app:forall a l, permI (a::l) (l++(a::nil))
|permI_trans:forall l1 l2 l3,
permI l1 l2 -> permI l2 l3 -> permI l1 l3.
Lemma counterexample : ~ permI (2::3::5::5::8::7::4::nil)
(3::2::8::7::4::3::5::nil).