proposition: Lemma reflects_conj {b1 b2 P1 P2} : reflects b1 P1 -> reflects b2 P2 -> reflects (b1 && b2) (P1 /\ P2).
proof: Proof. unfold reflects. destruct b1, b2; cbn; firstorder congruence. Qed.
imports: Undecidability.Synthetic.Definitions Lia Undecidability.Shared.Dec Setoid Morphisms