proposition: Theorem Permutation_ind_bis : forall P : list A -> list A -> Prop, P [] [] -> (forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) -> (forall x y l l', Permutation l l' -> P l l' -> P (y :: x :: l) (x :: y :: l')) -> (forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') -> forall l l', Permutation l l' -> P l l'.
proof: Proof. intros P Hnil Hskip Hswap Htrans. induction 1; auto. - apply Htrans with (x::y::l); auto. + apply Hswap; auto. induction l; auto. + apply Hskip; auto. apply Hskip; auto. induction l; auto. - eauto. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat