proposition: Lemma discrete_option X : discrete X -> discrete (option X).
proof: Proof. intros [d1] % discrete_iff. eapply discrete_iff. econstructor. unfold dec. decide equality. apply d1. Qed.
imports: Undecidability.Synthetic.Definitions Lia Undecidability.Shared.Dec Setoid Morphisms