ninductive t_byte8 (m:mcu_type) : Type ≝
TByte : byte8 → t_byte8 m.
-nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2.
- #m; #b1; #b2; #H;
- nchange with (match TByte m b2 with [ TByte a ⇒ b1 = a ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
+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 ≝