proposition: Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a].
proof: Proof. intros a l H; remember [a] as m in H. induction H; try (injection Heqm as [= -> ->]); discriminate || auto. apply Permutation_nil in H as ->; trivial. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat