proposition: Lemma decidable_iff' X p : {f | decider f p} -> (forall x : X, dec (p x)).
proof: Proof. intros [f H]. intros x. specialize (H x). destruct (f x); firstorder congruence. Qed.
imports: Undecidability.Synthetic.Definitions Lia Undecidability.Shared.Dec Setoid Morphisms