proposition: Lemma enumerator__T_sigT2 {X: Type} {P : X -> Type} {Q : X -> Type} f fP fQ : enumerator__T f X -> (forall x, enumerator__T (fP x) (P x)) -> (forall x, enumerator__T (fQ x) (Q x)) -> enumerator__T (sigT2_enum f fP fQ) {x : X & P x & Q x}.
proof: Proof. intros Hf HfP HfQ [x HPx HQx]. destruct (Hf x) as [nx Hnx]. destruct (HfP x (HPx)) as [nP HnP]. destruct (HfQ x (HQx)) as [nQ HnQ]. exists (Cantor.to_nat (nx, Cantor.to_nat (nP, nQ))). unfold sigT2_enum. now rewrite !Cantor.cancel_of_to, Hnx, HnP, HnQ. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia