fix probable error in definition of evaluate_ctxt
prove a cheat in one_step_backward
prove cheats in one_step_backward
prove cheats in one_step_backward_type_error