ndefinition word16_is_comparable_ext ≝ cn_is_comparable_ext byte8_is_comparable_ext.
unification hint 0 ≔ ⊢ carr (comp_base word16_is_comparable_ext) ≡ comp_num (comp_num exadecim).
unification hint 0 ≔ ⊢ carr (comp_base word16_is_comparable_ext) ≡ comp_num byte8.
unification hint 0 ≔ ⊢ carr (comp_base word16_is_comparable_ext) ≡ word16.
ndefinition word16_is_comparable_ext ≝ cn_is_comparable_ext byte8_is_comparable_ext.
unification hint 0 ≔ ⊢ carr (comp_base word16_is_comparable_ext) ≡ comp_num (comp_num exadecim).
unification hint 0 ≔ ⊢ carr (comp_base word16_is_comparable_ext) ≡ comp_num byte8.
unification hint 0 ≔ ⊢ carr (comp_base word16_is_comparable_ext) ≡ word16.