(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
ninductive MA_check : instr_mode → Type ≝
maINH : MA_check MODE_INH
(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
ninductive MA_check : instr_mode → Type ≝
maINH : MA_check MODE_INH