proposition: Lemma reflects_not b P : reflects b P -> reflects (negb b) (~P).
proof: Proof. unfold reflects. destruct b; cbn; intuition congruence. Qed.
imports: Undecidability.Synthetic.Definitions Lia Undecidability.Shared.Dec Setoid Morphisms