Library Cantor.prelude.decidable_set



Module Type S.

Parameter A : Set.
Axiom eq_A_dec : ∀ a1 a2 : A, {a1 = a2} + {a1 ≠ a2}.

End S.