Hola Carlos, muchas gracias por tu respuesta, buscando diferencias con el código que publicaste, pude encontrar el problema:
Inductive I: Set:=
| SKIP : I
| ASIGN : I
| BEGEND: LI->I
with LI:=
LI_NIL : LI.
Declaro el tipo de I como "Set" pero no el de LI, en el código que pasaste no declaras en niguno, parece que si declaras uno si y uno no arma lío =P, muchas gracias, tema solucionado.
Saludos.