strengthen compile_dec_thm, and bit more of compile_decs_thm