reprove compile_dec_thm (now with tuples)

the tuple constructor makes things nicer!