proposition: Theorem Permutation_app_inv (l1 l2 l3 l4:list A) a : Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4).
proof: Proof. intros. eapply Permutation_Add_inv; eauto using Add_app. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat