+definition mb_chk_get ≝
+λchk:Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type)))).λaddr:word16.
+let c ≝ mt_visit (Prod8T memory_type) chk addr in
+array_8T ? (getn_array8T o7 ? c) (getn_array8T o6 ? c)
+ (getn_array8T o5 ? c) (getn_array8T o4 ? c)
+ (getn_array8T o3 ? c) (getn_array8T o2 ? c)
+ (getn_array8T o1 ? c) (getn_array8T o0 ? c).
+