proposition: Lemma permut_nil : forall l, permutation l [] -> l = [].
proof: Proof. intro l; destruct l as [ | e l ]; trivial. assert (InA eqA e (e::l)) by (auto with *). intro Abs; generalize (permut_InA_InA Abs H). inversion 1. Qed.
imports: Lia Relations Multiset SetoidList