Hola.
No es la idea usar List. Si defenís:
Inductive I :=
| skip: I
| ...
| begin_end : LI -> I
with LI :=
| nilLI: LI
| consLI: I -> LI ->LI.
Lo que se pide en el 6.2 sería (por ejemplo):
Infix "::" := consLI (at level 60, right associativity).
Saludos, Carlos