- [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T ????? c1') (fst5T ????? c2')) ⊗
- (eq_anyop m (snd5T ????? c1') (snd5T ????? c2')) ⊗
- (eq_instrmode (thd5T ????? c1') (thd5T ????? c2')) ⊗
- (eq_b8 (frth5T ????? c1') (frth5T ????? c2')) ⊗
- (eq_w16 (ffth5T ????? c1') (ffth5T ????? c2')) ]
+ [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T … c1') (fst5T … c2')) ⊗
+ (eq_anyop m (snd5T … c1') (snd5T … c2')) ⊗
+ (eq_im (thd5T … c1') (thd5T … c2')) ⊗
+ (eq_b8 (frth5T … c1') (frth5T … c2')) ⊗
+ (eq_w16 (ffth5T … c1') (ffth5T … c2')) ]