proposition: Lemma sort_equivlistA_eqlistA : forall l l' : list elt, sort E.lt l -> sort E.lt l' -> equivlistA E.eq l l' -> eqlistA E.eq l l'.
proof: Proof. apply SortA_equivlistA_eqlistA; auto with typeclass_instances. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide