Hola, ¿la idea de este ejercicio es utilizar como testigo la función insert_sort? Sin embargo dicha función toma cómo primer parámetro un elemento, ¿la idea es probar que para todo elemento se cumple la especificación? Es decir poner el forall en el lemma.
Saludos,
Jairo.
Hola.
La función insert_sort del práctico 4 (ej. 4.6.3) dada una lista (no hay elementos) retorna la lista ordenada.
Esta función seguramente usa como auxiliar otra que dada una lista ordenada y un elemento retorna la lista ordenada que lo incluye.
El problema es tratado en el libro Coq'Art.
Saludos, Carlos