- mk_Array8T ? (fst4T … (bits_of_exadecim (b8h b)))
- (snd4T … (bits_of_exadecim (b8h b)))
- (thd4T … (bits_of_exadecim (b8h b)))
- (fth4T … (bits_of_exadecim (b8h b)))
- (fst4T … (bits_of_exadecim (b8l b)))
- (snd4T … (bits_of_exadecim (b8l b)))
- (thd4T … (bits_of_exadecim (b8l b)))
- (fth4T … (bits_of_exadecim (b8l b))).
+ mk_Array8T ? (fst4T … (bits_of_exadecim (cnH ? b)))
+ (snd4T … (bits_of_exadecim (cnH ? b)))
+ (thd4T … (bits_of_exadecim (cnH ? b)))
+ (fth4T … (bits_of_exadecim (cnH ? b)))
+ (fst4T … (bits_of_exadecim (cnL ? b)))
+ (snd4T … (bits_of_exadecim (cnL ? b)))
+ (thd4T … (bits_of_exadecim (cnL ? b)))
+ (fth4T … (bits_of_exadecim (cnL ? b))).