Hello,

I am trying to test simple conjecture with QuickChick:

```
Conjecture lists_eq : forall (l : list string), l = l.
QuickChick lists_eq.
```

but I get this error:

*Unable to satisfy the following constraints: ?arg_2 : “Checkable (forall l : list string, l = l)”*

I know I need to make my property Instance of class Checkable, but how should I do it?

I made decidability on two lists (successfully) *Instance EqLists_Dec (x y : list string) : Dec (x = y).*

I made Arbitrary for list (successfully) Instance gen_list_string : Gen (list string)

But I couldn’t make Property checkable, I know that bool type is Checkable in QC.

Here is the code, plese advice. Maybe I am doing it all in a wrong way.

```
From QuickChick Require Import QuickChick.
Require Import List ZArith. Import ListNotations.
Import QcNotation.
Set Warnings "-extraction-opaque-accessed,-extraction".
Require Import String. Local Open Scope string.
Definition genListString : G (list string) :=
elems_ ["Two" ; "Three"]
[
[ "One" ; "Nstasss" ; "SomeStr" ; "Yellow" ];
[ "111" ; "2222" ; "33333SomeStr" ; "44444Yellow" ]
].
(* Sample genListString. *)
Instance gen_list_string : Gen (list string) :=
{
arbitrary := genListString
}.
Notation "P '?'" :=
(match (@dec P _) with
| left _ => true
| right _ => false
end)
(at level 100).
Instance EqLists_Dec (x y : list string) : Dec (x = y).
Proof. dec_eq. Defined.
(* Problem in this function, couldn't make it work*)
Instance checkableDec `{P : Prop} `{Dec P} : Checkable P :=
{
checker p := if P? then ret ok else ret Failure
}.
Conjecture lists_eq : forall (l : list string), l = l.
QuickChick lists_eq.
(*
Unable to satisfy the following constraints:
?arg_2 : "Checkable (forall l : list string, l = l)"
*)
```

I also asked same question on StackOverflow :