fact: Definition discriminable_type := { D & { _ : discrete D & { _ : finite_t D & { δ : X -> D | forall x y, x ≡ y <-> δ x = δ y } } } }.
imports: List Bool Undecidability.Shared.Libs.DLW.Utils(utils_list finite fin_quotient fin_dec utils_decidable) Undecidability.FOL.TRAKHTENBROT(notations utils decidable)