fact: Definition to_list_enum {X} (f : nat -> option X) := (fun n : nat => match f n with | Some x => [x] | None => [] end) .
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts ListEnumerabilityFacts) Lia Undecidability.L(LProd LBool LNat LOptions) Undecidability.L.Datatypes.List(List_basics List_eqb List_extra List_nat)