Equality on unordered pairs
Let t:Set be a type with an equivalence relation
eq:t->t->Prop. We can represent unordered pairs of elements of
as elements of the cartesian product t*t, considering
the pairs (x,y) and (y,x) as equivalent.
Moreover, if eq is decidable, the equivalence on t*t induced
induced by eq and satisfying the property above is decidable too.
Express this construction by a functor taking as argument an arbitrary module
M:DecidableType (see Coq's standard library).
Solution
Follow this link
Going home