inductive any_opcode (m:mcu_type) : Type ≝
anyOP : opcode → any_opcode m.
-coercion anyOP.
+definition c_anyOP ≝ anyOP.
+
+coercion c_anyOP.
(* raggruppamento di byte e word in un tipo unico *)
inductive byte8_or_word16 : Type ≝
Byte: byte8 → byte8_or_word16
| Word: word16 → byte8_or_word16.
-coercion Byte.
-coercion Word.
+definition c_Byte ≝ Byte.
+definition c_Word ≝ Word.
+
+coercion c_Byte.
+coercion c_Word.
(* opcode → naturali, per usare eqb *)
definition magic_of_opcode ≝