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