split off Basics/Decidable.v, with a few new lemmas in it

Is this NB still relevant? It got copied from `Overture`.