proposition: Theorem Permutation_sym : forall l l' : list A, Permutation l l' -> Permutation l' l.
proof: Proof. intros l l' Hperm; induction Hperm; auto. apply perm_trans with (l':=l'); assumption. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat