proposition: Lemma enumerator__T_sum {X Y} f1 f2 : enumerator__T f1 X -> enumerator__T f2 Y -> enumerator__T (sum_enum f1 f2) (X + Y).
proof: Proof. intros H1 H2 [x|y]. - destruct (H1 x) as [m Hm]. exists (Cantor.to_nat (0, m)). unfold sum_enum. now rewrite Cantor.cancel_of_to, Hm. - destruct (H2 y) as [m Hm]. exists (Cantor.to_nat (1, m)). unfold sum_enum. now rewrite Cantor.cancel_of_to, Hm. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia