proposition: Lemma dec_compl' X p : decidable (fun x : X => ~ ~ p x) -> decidable (fun x : X => ~ p x).
proof: Proof. intros [f H]. exists (fun x => negb (f x)). intros x. specialize (H x). apply reflects_not in H. unfold reflects in *. tauto. Qed.
imports: Undecidability.Synthetic.Definitions Lia Undecidability.Shared.Dec Setoid Morphisms