proposition: Lemma enumerator__T_prod {X Y} f1 f2 : enumerator__T f1 X -> enumerator__T f2 Y -> enumerator__T (prod_enum f1 f2) (X * Y).
proof: Proof. intros H1 H2 (x, y). destruct (H1 x) as [n1 Hn1], (H2 y) as [n2 Hn2]. exists (Cantor.to_nat (n1, n2)). unfold prod_enum. now rewrite Cantor.cancel_of_to, Hn1, Hn2. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia