Thank you. But then I have another problem in using foo together with functions in FSetInterface.S.

In the following code, the lemma test cannot be defined.

The error message is: The term “x” has type “S.elt” while it is expected to have type “S.E’.t”.

```
Module Lemmas (S : NewSet).
Lemma test :
forall (x y : S.elt) (s : S.t),
S.mem x s = S.mem y s -> S.E'.foo x y = true.
Proof.
Admitted.
End Lemmas.
```

In the following code, the lemma test cannot be defined.

The error message is: The term “x” has type “S.E’.t” while it is expected to have type “S.elt”.

```
Module Lemmas (S : NewSet).
Lemma test :
forall (x y : S.E'.t) (s : S.t),
S.mem x s = S.mem y s -> S.E'.foo x y = true.
Proof.
Admitted.
End Lemmas.
```

In the following code, lemma test cannot be defined.

The error message is: The term “x” has type “O.t” while it is expected to have type “S.elt”.

```
Module Lemmas (O : NewOT) (S : NewSet with Module E' := O).
Lemma test :
forall (x y : O.t) (s : S.t),
S.mem x s = S.mem y s -> O.foo x y = true.
Proof.
Admitted.
End Lemmas.
```

In the following code, NewNatLemmas cannot be defined.

The error message is: Error: The field foo is missing in Top.NewNatSet.E.

```
Module Lemmas (O : NewOT) (S : NewSet with Module E' := O with Module E := O).
Lemma test :
forall (x y : O.t) (s : S.t),
S.mem x s = S.mem y s -> O.foo x y = true.
Proof.
Admitted.
End Lemmas.
From Coq Require Import OrderedTypeEx.
Module NewNatOT <: NewOT.
Include Nat_as_OT.
Definition foo := Nat.eqb.
End NewNatOT.
Module NewNatSet := Make' NewNatOT.
Module NewNatLemmas := Lemmas NewNatOT NewNatSet.
```

My current solution is to re-define Backport_Sets and use it instead of FSetList.Make.

But I wonder if there is more elegant way to solve the problem.