proposition: Lemma dec_disj X p q : decidable p -> decidable q -> decidable (fun x : X => p x \/ q x).
proof: Proof. intros [f] [g]. exists (fun x => orb (f x) (g x)). intros x. eapply reflects_disj; eauto. Qed.
imports: Undecidability.Synthetic.Definitions Lia Undecidability.Shared.Dec Setoid Morphisms