Buenas,
Pongo el ejercicio ocho como ejemplo pero la duda es más en general.
Me resulta muy curioso que Coq me deje escribir
forall (n : nat), Array' bool n
pero no
Array' bool
cuando se supone deberían tener el mismo tipo.
Tengo una vaga idea de qué es la impredicatividad pero no me siento súper cómodo con el concepto. Va por ahí el problema?
Gracias.