inductive any_opcode (m:mcu_type) : Type ≝
anyOP : opcode → any_opcode m.
-coercion cic:/matita/freescale/opcode/any_opcode.ind#xpointer(1/1/1).
+coercion 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 cic:/matita/freescale/opcode/byte8_or_word16.ind#xpointer(1/1/1).
-coercion cic:/matita/freescale/opcode/byte8_or_word16.ind#xpointer(1/1/2).
+coercion Byte.
+coercion Word.
(* opcode → naturali, per usare eqb *)
definition magic_of_opcode ≝