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