fact: Definition SetEq {A: Type} (seq1: list A) (seq2: list A) := forall x, List.In x seq1 <-> List.In x seq2.
imports: Coq.Lists.List Coq.Bool.Bool Coq.Structures.OrderedType Coq.Classes.Morphisms Coq.Setoids.Setoid Fiat.Common.Coq__8_4__8_5__Compat