proposition: Lemma Permutation_length_1: forall a b, Permutation [a] [b] -> a = b.
proof: Proof. intros a b H. apply Permutation_length_1_inv in H; injection H as [= ->]; trivial. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat