proposition: Theorem permutation_nil_inv : forall l : list A, permutation l nil -> l = nil.
proof: Proof. intros l H; generalize (permutation_length _ _ H); case l; simpl in |- *; auto. intros; discriminate. Qed.
imports: List ListAux