Library prelude.decidable_set

Module Type S.

Parameter A : Set.
Axiom eq_A_dec : forall a1 a2 : A, {a1 = a2} + {a1 <> a2}.

End S.