proposition: Theorem Permutation_app_inv_l : forall l l1 l2, Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2.
proof: Proof. induction l; simpl; auto. intros. apply IHl. apply Permutation_cons_inv with a; auto. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat