proposition: Theorem Permutation_cons_inv l l' a : Permutation (a::l) (a::l') -> Permutation l l'.
proof: Proof. intro. eapply Permutation_Add_inv; eauto using Add_head. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat