update mkshift_thm
more thoughts about new exp_to_Cexp_correct

looks like will need to reason about free variables, and therefore
probably also closed values.