# Library FiniteSets

```
```

A library for finite sets with extensional equality.

Author: Brian Aydemir.

Author: Brian Aydemir.

```
```

Require Import FSets.

Require Import ListFacts.

```
```

The following interface wraps the standard library's finite set
interface with an additional property: extensional equality.

```
```

Module Type S.

Declare Module E : UsualOrderedType.

Declare Module F : FSetInterface.S with Module E := E.

Parameter eq_if_Equal :

forall s s' : F.t, F.Equal s s' -> s = s'.

End S.

```
```

For documentation purposes, we hide the implementation of a
functor implementing the above interface. We note only that the
implementation here assumes (as an axiom) that proof irrelevance
holds.

```
```

Module Make (X : UsualOrderedType) <: S with Module E := X.

End Make.