vacio ---> es un ejemplo del uso de la táctica inversion. Cuando se 
tiene en el contexto un término de un tipo inductivo que resulta 
imposible de construir con los constructores de dicho tipo, entonces se 
puede probar el objetivo.

concatenacion ---> distintas maneras de definir la concatenacion de 
listas y su equivalencia.

ejercicio2_3.v ---> es una posible solución a los ejercicios no 
resueltos del coq in a hurry.
 
