Hola.
Las variables en este problema en este ejercicio están definidas con números naturales. Para los programas concretos podés declarar variables Coq para v1, v2, aux... (que son números naturales: Variables v1 v2 aux : Var). Otra alternativa es definir estos programas para que reciban como parámetro a las variables involucradas.
Respecto a valores indefinidos, paso lo mismo que en los programas reales. En el ejemplo v1 es de tipo Var (nat). Fijate por ejemplo que para probar cierta propiedad sobre el programa PP se pide que las variables involucradas sean distintas (esto se plantea en la formulación de un lema).
Saludos, Carlos