proposition: Lemma decidable_iff X p : decidable p <-> inhabited (forall x : X, dec (p x)).
proof: Proof. split. - intros [f H]. econstructor. intros x. specialize (H x). destruct (f x); firstorder congruence. - intros [d]. eapply dec_decidable' in d as [f]. now exists f. Qed.
imports: Undecidability.Synthetic.Definitions Lia Undecidability.Shared.Dec Setoid Morphisms