proposition: Lemma SetEq_rewrite : forall {A: Type} (seq1 seq2: list A), SetEq seq1 seq2 <-> forall a, List.In a seq1 <-> List.In a seq2.
proof: Proof. unfold SetEq; tauto. Qed.
imports: Coq.Lists.List Coq.Bool.Bool Coq.Structures.OrderedType Coq.Classes.Morphisms Coq.Setoids.Setoid Fiat.Common.Coq__8_4__8_5__Compat