Complete conversion of simp module

Some functions on simpset are unsafe. They may be converted later.