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