proposition: Lemma dec_decidable' X p : (forall x : X, dec (p x)) -> { f : _ | forall x, p x <-> f x = true}.
proof: Proof. intros d. exists (fun x => if d x then true else false). intros x. destruct (d x); firstorder congruence. Qed.
imports: Undecidability.Synthetic.Definitions Lia Undecidability.Shared.Dec Setoid Morphisms