proposition: Fact discernable_undiscernable x y : x ≢ y -> x ≡ y -> False.
proof: Proof. intros (f & Hf) H; apply Hf, H. Qed.
imports: List Bool Undecidability.Shared.Libs.DLW.Utils(utils_list finite fin_quotient fin_dec utils_decidable) Undecidability.FOL.TRAKHTENBROT(notations utils decidable)