ninductive t_byte8 (m:mcu_type) : Type ≝
TByte : byte8 → t_byte8 m.
+ndefinition eq_tbyte8 ≝
+λm.λtb1,tb2:t_byte8 m.
+ match tb1 with
+ [ TByte b1 ⇒ match tb2 with
+ [ TByte b2 ⇒ eq_b8 b1 b2 ]].
+
(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
ninductive MA_check : instr_mode → Type ≝
maINH : MA_check MODE_INH