fact: Definition of_list_enum {X} (f : nat -> list X) := (fun n : nat => let (n0, m) := Cantor.of_nat n in nth_error (f n0) m).
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)