We can use the substitution rules to produce a nicer version. Thinking of return (x,y) as a function of y and applying rule 2 gives