proposition: Theorem Permutation_nil : forall (l : list A), Permutation [] l -> l = [].
proof: Proof. intros l HF. remember (@nil A) as m in HF. induction HF; discriminate || auto. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat