proposition: Lemma enumerator__T_option {X} f : enumerator__T f X -> enumerator__T (option_enum f) (option X).
proof: Proof. intros H [x | ]. - destruct (H x) as [n Hn]. exists (S n). cbn. now rewrite Hn. - exists 0. reflexivity. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia