Hola Juan Manuel.
Las versiones de Coq van cambiando rápido...
Lo que decís está bien, asi que adelante con esa estrategia. En la versión que tengo instalada (que no es la última) esto es un poco distinto. Mientrass que funcione en alguna versión de Coq está bien, ya que la idea es que experimenten la extracción, simplemente.
Saludos, Carlos