start on updating compile_dec theorem

removing the mn = NONE hypothesis makes some subgoals in the case for a
type declaration harder - cheating for now.

will also need theorems about compile_decs and compile_top.