Hello!

I suspect the answer to this question is “no”, but can `FSets`

have decidable Leibniz equality given elements that have decidable Leibniz equality? A simple example with `nat`

:

```
Require Import Coq.FSets.FSetInterface.
Require Import Coq.FSets.FSetWeakList.
Require Import Coq.FSets.FSetFacts.
Require Import Coq.Structures.Equalities.
Require Import Coq.Arith.PeanoNat.
(** A mini decidable type module to instantiate sets. *)
Module NatMiniDec : MiniDecidableType
with Definition t := nat.
Definition t := nat.
Definition eq := @Logic.eq t.
Definition eq_refl := @Logic.eq_refl t.
Definition eq_sym := @Logic.eq_sym t.
Definition eq_trans := @Logic.eq_trans t.
Theorem eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
Proof. apply Nat.eq_dec. Qed.
End NatMiniDec.
(** A usual decidable type module to instantiate sets. *)
Module NatDec <: UsualDecidableType
with Definition t := nat
with Definition eq := @Logic.eq nat
:= Make_UDT NatMiniDec.
(** A Sets module with nats. *)
Module NatSets : FSetInterface.WS
with Definition E.t := nat
with Definition E.eq := @Logic.eq nat
:= FSetWeakList.Make NatDec.
Theorem dec : forall (s0 s1 : NatSets.t),
{s0 = s1}+{~s0 = s1}.
Proof.
Fail decide equality.
Print NatSets.eq_dec.
Print NatSets.eq.
Print NatSets.Equal.
Abort.
```

We can see that there’s a `NatSets.eq_dec`

, but it’s defined in terms of `NatSets.Equal`

, which isn’t Leibniz.

Normally I wouldn’t care, but I have a structure for which I want decidable Leibniz equality, and that structure just happens to contain a NatSets.t somewhere in it.