proposition: Fact undiscernable_Prop_dec x y : x ≡ y -> forall P, (forall x, decidable (P x)) -> P x <-> P y.
proof: Proof. intros H P HP. set (f x := if HP x then true else false). specialize (H f); unfold f in H. destruct (HP x); destruct (HP y); try tauto; 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)