Buenas! Estaba poniendo Extraction Language Haskell tal como sugiere el practico pero me da Syntax error: illegal begin of vernac. No entiendo por que puede suceder ni como resolverlo.
Otra consulta que tengo es en el ejercicio 2. Defini inverse y luego estaba intentando probar el Lemma MirrorCI : forall (A : Set) (t : bintree A), {t2 : bintree A | mirror A t t2}.
Para esto hice intros. exists (inverse A t). Aqui me gustaria usar functional induction (inverse A t) como sugiere el practico, pero me dice "The reference functional was not found in the current environment."