fact: Definition prod_enum {X Y} (f1 : nat -> option X) (f2 : nat -> option Y) n : option (X * Y) := let (n, m) := Cantor.of_nat n in if! (f1 n, f2 m) is (Some x, Some y) then Some (x, y) else None.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia