+nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y).
+ #x; #y;
+ nnormalize;
+ nelim x;
+ nelim y;
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (exadecim_destruct … H)
+ ##]
+nqed.
+