(* **************************************** *)
(* raccordo di tutte le possibili scritture *)
(* **************************************** *)
ndefinition multi_mode_writeb ≝
λm.match m
(* **************************************** *)
(* raccordo di tutte le possibili scritture *)
(* **************************************** *)
ndefinition multi_mode_writeb ≝
λm.match m