proposition: Theorem Permutation_cons_app_inv l l1 l2 a : Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2).
proof: Proof. intro. eapply Permutation_Add_inv; eauto using Add_head, Add_app. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat