fact: Definition option_enum {X} (f : nat -> option X) n := match n with 0 => Some None | S n => Some (f n) end.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia