proposition: Lemma SetEq_modulo_SetEqSafe_fun : forall {A B: Type}, forall (seq1: list B) (seq2 seq3: list A), forall (proc: list A -> list B), SetEq seq2 seq3 -> IsSetEqSafe proc -> (SetEq seq1 (proc seq2) <-> SetEq seq1 (proc seq3)).
proof: Proof. intros; eauto using SetEq_trans_iff_2. Qed.
imports: Coq.Setoids.Setoid Coq.Lists.List Coq.Sorting.Permutation Fiat.Common.List.FlattenList Fiat.Common.SetEq