Hello!

I have the following file:

```
Require Coq.FSets.FMaps.
Require Coq.FSets.FMapAVL.
Require Coq.Strings.String.
Require Coq.Structures.OrderedTypeEx.
Module Maps : FMapInterface.S with Definition E.t := String.string :=
FMapAVL.Make OrderedTypeEx.String_as_OT.
(* Maps.E.t = String.string *)
Print Maps.E.t.
(* eq = Logic.eq *)
Print OrderedTypeEx.String_as_OT.eq.
(* eq = ??? *)
Print Maps.E.eq.
Lemma k : forall m n, Maps.E.eq m n -> m = n.
Proof.
intros m n Heq.
(* setoid rewrite failed *)
rewrite Heq.
```

I’m trying to work backwards to determine why exactly the rewrite fails with a pretty obnoxious looking rewrite failure:

```
Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
?X9==[m n Heq |- Relation_Definitions.relation Maps.E.t] (internal placeholder) {?r}
?X10==[m n Heq (do_subrelation:=Morphisms.do_subrelation)
|- Morphisms.Proper (Morphisms.respectful Maps.E.eq (Morphisms.respectful ?r (Basics.flip Basics.impl)))
eq] (internal placeholder) {?p}
?X11==[m n Heq |- Morphisms.ProperProxy ?r n] (internal placeholder) {?p0}
TYPECLASSES:?X9 ?X10 ?X11
SHELF:||
FUTURE GOALS STACK:?X11 ?X10 ?X9||?X3 ?X2 ?X1
.
```

Firstly:

```
Module Maps : FMapInterface.S with Definition E.t := String.string :=
```

I’m using `: FMapInterface.S`

because I want the internals of `Maps`

to be abstracted away as much as possible; I don’t want proofs over `Maps.t`

to descend into the guts of the AVL tree; I want to work solely from the exposed `Maps`

and `FMapFacts`

theorems. However, I think this causes an issue because:

```
(* Maps.E.t = String.string *)
Print Maps.E.t.
(* eq = Logic.eq *)
Print OrderedTypeEx.String_as_OT.eq.
(* eq = ??? *)
Print Maps.E.eq.
```

… Although `Maps.E.t`

is exposed as `string`

thanks to the `with`

clause, and `OrderedTypeEx.String_as_OT.eq`

is visible as Leibniz equality, the `Maps.E.eq`

definition appears to Coq to be an arbitrary `t -> t -> Prop`

function. The failed proof of `k`

would seem to confirm this. If I instead use:

```
Module Maps <: FMapInterface.S with Definition E.t := String.string :=
```

The rewrite works as the concrete definition of `eq`

is exposed, but then proofs involving `Maps.t`

are exposed to the fact that it’s an AVL tree because the concrete details of *everything else* in the module are exposed too.

I feel like this is a case of needing generalized rewriting, which I (unfortunately) don’t know how to use yet and I’m still struggling through the documentation for it.

Is there a pleasant way to get `Maps.E.eq`

to work in rewrites without using `<:`

?