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