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