refactor(library): mark 'decidable' theorems as definitions

If we don't do that, then any 'if' term that uses one of these theorems
will get "stuck". That is, the kernel will not be able to reduce them
because theorems are always opaque
refactor(library): mark 'decidable' theorems as definitions