Hi, I'im trying to prove the equality for an *slist* of inductive types, but I cannot prove it unless I know that X is decidable, but how can I tell to Coq that X is decidable in *eq_dec_slist* proposition?

```
Inductive slist (X: Type): Type :=
| empty : slist X
| snoc : slist X -> X -> slist X.
Arguments empty {X}.
Arguments snoc {X} _ _.
Proposition eq_dec_slist (X: Type) (G G': slist X): {G = G'} + {G <> G'}.
Proof.
intros.
decide equality.
Abort.
```

you should add it as an hypothesis:

```
Proposition eq_dec_slist (X: Type) (deceqX : forall x x' : X, {x = x'} + {x <> x'}) (G G': slist X): {G = G'} + {G <> G'}.
Proof.
intros.
decide equality.
Defined.
```

Last updated: Jun 16 2024 at 03:41 UTC