Hello,

I am trying to represent associative lists “list (key * value)” where the type of “value” may depend on “key” and define a predicate that asserts that a given pair `(key, value)`

belongs to the association list. My first idea was to define

```
Inductive Assoc {A : Type} {B : A -> Type} (a : A) (u : B a) : list (sigT B) -> Prop :=
| Ass_hd: forall xs,
Assoc a u (existT _ a u :: xs)
| Ass_tl: forall x xs,
Assoc a u xs ->
Assoc a u (x :: xs).
```

The problem is that I need to use this when `A`

has a specific notion of equality (eg `A = Q`

). Hence, I want the above definition of `Assoc`

extended so that the following property holds:

```
Parameter eq : A -> A -> Prop.
forall a b u xs, eq a b -> (Assoc a u xs <-> Assoc b u xs).
```

This looks like it would require considering compatibilities between `eq`

and `B`

(eg `eq x y -> B x = B y`

), and it looks quite complicated in general. Is there a better way? How can I make this work?

Thanks!