(l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
match l with
[ nil ⇒ c
| cons hd tl ⇒ match fst4T ???? hd with
[ anyOP o' ⇒ match eqop m (anyOP m o) (anyOP m o') with
(l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
match l with
[ nil ⇒ c
| cons hd tl ⇒ match fst4T ???? hd with
[ anyOP o' ⇒ match eqop m (anyOP m o) (anyOP m o') with