proposition: Theorem Permutation_nil_cons : forall (l : list A) (x : A), ~ Permutation nil (x::l).
proof: Proof. intros l x HF. apply Permutation_nil in HF; discriminate. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat