Hola.
Si, me refiero a los ejercicios que no tienen intros (uno en el 14 y los últimos en el 15).
Por ejemplo, la función identidad sobre un tipo A (fun x:A => x) es un término de prueba de A->A. Luego, el término de prueba que construye la táctica intro es una lambda abstracción.
Saludos Carlos