fact: Fixpoint enc {k} i (v : Vector.t nat k) : nat := match v with | @Vector.nil _ => 1 | x :: v => (qs i) ^ x * enc (S i) v end.
imports: Vector List Arith Undecidability.Shared.Libs.DLW(gcd rel_iter pos vec) Undecidability.FRACTRAN(prime_seq)