proposition: Fact discernable_dec_undiscernable_dec x y : decidable (x ≡ y).
proof: Proof. Proof using H2. destruct (H2 x y); [ right | left ]; rewrite undiscernable_spec; tauto. Qed.
imports: List Bool Undecidability.Shared.Libs.DLW.Utils(utils_list finite fin_quotient fin_dec utils_decidable) Undecidability.FOL.TRAKHTENBROT(notations utils decidable)