proposition: Fact undiscernable_discrete D (δ : X -> D) x y : discrete D -> x ≡ y -> δ x = δ y.
proof: Proof. intros d H. set (g z := if d (δ x) (δ z) then true else false). specialize (H g); unfold g in H. destruct (d (δ x) (δ x)) as [ _ | [] ]; auto. destruct (d (δ x) (δ y)) as [ | ]; easy. Qed.
imports: List Bool Undecidability.Shared.Libs.DLW.Utils(utils_list finite fin_quotient fin_dec utils_decidable) Undecidability.FOL.TRAKHTENBROT(notations utils decidable)