proposition: Lemma SetEq_append : forall {A: Type} (seq1 seq2: list A) (x: A), SetEq seq1 seq2 -> SetEq (x :: seq1) (x :: seq2).
proof: Proof. intros A s1 s2 x s_eq; unfold SetEq; split; intro H; simpl in *; [rewrite s_eq in H | rewrite <- s_eq in H]; intuition. Qed.
imports: Coq.Setoids.Setoid Coq.Lists.List Coq.Sorting.Permutation Fiat.Common.List.FlattenList Fiat.Common.SetEq