inductive t_byte8 (m:mcu_type) : Type ≝
TByte : byte8 → t_byte8 m.
-coercion TByte.
+definition c_TByte ≝ TByte.
+
+coercion c_TByte.
(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
inductive MA_check : instr_mode → Type ≝
inductive instruction : Type ≝
instr: ∀i:instr_mode.opcode → MA_check i → instruction.
-coercion instr.
+definition c_instr ≝ instr.
+
+coercion c_instr.
(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
MA_check i → list (t_byte8 m) *)