reorganise file, and get decs_contab_thm proof working again
prove first case of a compile_dec_thm