proposition: Fact discrete_undiscernable_implies_equal x y : discrete X -> x ≡ y -> x = y.
proof: Proof. intro; now apply undiscernable_discrete with (δ := fun x => x). Qed.
imports: List Bool Undecidability.Shared.Libs.DLW.Utils(utils_list finite fin_quotient fin_dec utils_decidable) Undecidability.FOL.TRAKHTENBROT(notations utils decidable)