Hi. Within a section I can use

```
Parameter A : Type.
```

to assume `A`

to be a type. I would like to constrain `A`

so that it is any type with decidable equality. I found Coq.Structures.Equalities.HasEqDec but don’t know how to use it.

Hi. Within a section I can use

```
Parameter A : Type.
```

to assume `A`

to be a type. I would like to constrain `A`

so that it is any type with decidable equality. I found Coq.Structures.Equalities.HasEqDec but don’t know how to use it.

If you really want to use `Structures.Equalities`

, then just start your script with

```
Module Foo (Import M:MiniDecidableType).
```

You will then be in a context where there is a type `t`

with a decidable equality.

```
Goal forall x y:t, x = y \/ x <> y.
Proof.
intros x y.
destruct (eq_dec x y).
now left.
now right.
Qed.
```

But this is kind of overengineered. If you do not care about modules, just start your script with

```
Parameter t:Type.
Parameter eq_dec: forall x y:t, {x = y} + {x <> y}.
```

This has the exact same effect as before.

Thanks. I was also advised to assume more axioms and, more importantly, according to the advisor, to avoid using modules at all costs. I am going to learn more about the reason. For now this problem has a good enough solution.