proposition: Fact discernable_equiv1 x y : x ≢ y <-> exists δ, δ x = true /\ δ y = false.
proof: Proof. split. + intros (f & Hf). case_eq (f x); intros Hx. * exists f; split; auto. now rewrite Hx in Hf; destruct (f y). * exists (fun x => negb (f x)). rewrite Hx in *; split; auto. now destruct (f y). + intros (f & E1 & E2); exists f. now rewrite E1, E2. Qed.
imports: List Bool Undecidability.Shared.Libs.DLW.Utils(utils_list finite fin_quotient fin_dec utils_decidable) Undecidability.FOL.TRAKHTENBROT(notations utils decidable)