fact: Definition bool_enum (n : nat) := Some (if! n is 0 then true else false).
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia