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).