proposition: Lemma seteq_nil_nil : forall {A} seq, @SetEq A seq nil <-> seq = nil.
proof: Proof. unfold SetEq. intros; destruct seq. tauto. split; [ | discriminate ]. intro H; specialize (H a). exfalso; simpl in H; rewrite <- H; eauto. Qed.
imports: Coq.Setoids.Setoid Coq.Lists.List Coq.Sorting.Permutation Fiat.Common.List.FlattenList Fiat.Common.SetEq