proposition: Lemma SetEq_Equivalence: forall {A: Type}, Equivalence (SetEq (A:=A)).
proof: Proof. intros; constructor; seteq_equivalence. 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