blob: cc8739afe67acdf5ad088c7d6cb3ecad25c9c0b8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}.
Typeclasses eauto := debug.
Set Typeclasses Debug Verbosity 2.
Inductive Finx(n : nat) : Set :=
| Fx1(i : nat)(e : n = S i)
| FxS(i : nat)(f : Finx i)(e : n = S i).
Context `{Finx_eqdec : forall n, Eqdec (Finx n)}.
Goal {x : Type & Eqdec x}.
eexists.
try typeclasses eauto 1 with typeclass_instances.
|
