(* raggruppamento di byte e word in un tipo unico *)
inductive byte8_or_word16 : Type ≝
Byte: byte8 → byte8_or_word16
| Word: word16 → byte8_or_word16.
(* raggruppamento di byte e word in un tipo unico *)
inductive byte8_or_word16 : Type ≝
Byte: byte8 → byte8_or_word16
| Word: word16 → byte8_or_word16.