top_command (cmd_load currentFile [])
goal_command 0 cmd_refine "_+ x"
goal_command 1 cmd_refine "x +_"
goal_command 2 cmd_refine "_+ x"
goal_command 3 cmd_refine "λ z → z + x"
goal_command 4 cmd_refine "λ a b → b + x"
goal_command 5 cmd_refine "λ a → a + (a + x)"
goal_command 6 cmd_refine "λ a → x + (y + a)"
goal_command 7 cmd_refine "λ a b → a + b"
