fact: Definition Diophantine' {k} (R : Vector.t nat k -> nat -> Prop) : Prop := Diophantine (fun v : Vector.t nat (S k) => match v with cons _ m n v => fun R : Vector.t nat n -> nat -> Prop => R v m end R).
imports: Undecidability.H10.Dio(dio_single) Coq(List Vector Nat)