proposition: Lemma enumerator__T_Vector {X: Type} {k: nat} (f : nat -> option X) : enumerator__T f X -> enumerator__T (Vector_enum f) (Vector.t X k).
proof: Proof. intros Hf. induction k as [|k IH]. { intros t. pattern t. apply (Vector.case0). now exists 0. } intros t. rewrite (Vector.eta t). destruct (Hf (VectorDef.hd t)) as [nx Hnx]. destruct (IH (VectorDef.tl t)) as [m Hm]. exists (Cantor.to_nat (nx, m)). cbn. now rewrite Cantor.cancel_of_to, Hnx, Hm. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia