proposition: Fact find_discrete_projection y : { x | x ∊ l /\ f x = y } + (forall x, x ∊ l -> f x <> y).
proof: Proof. Proof using HY. destruct list_choose_dep with (P := fun x => f x = y) (Q := fun x => f x <> y) (l := l) as [ (? & ? & ?) | ]; eauto. intros; apply HY. Qed.
imports: List Bool Undecidability.Synthetic(Definitions ReducibilityFacts InformativeDefinitions InformativeReducibilityFacts) Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_decidable finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils decidable discernable fol_ops fo_sig fo_terms fo_logic fo_sat Sig1_1 red_utils)