λbw1,bw2:byte8_or_word16.
match bw1 with
[ Byte b1 ⇒ match bw2 with [ Byte b2 ⇒ eq_b8 b1 b2 | Word _ ⇒ false ]
- | Word w1 ⇒ match bw2 with [ Byte _ ⇒ false | Word w2 ⇒ eq_w16 w1 w1 ]
+ | Word w1 ⇒ match bw2 with [ Byte _ ⇒ false | Word w2 ⇒ eq_w16 w1 w2 ]
].