• Suppose we have a recursive function:

fAux x y =   if (cond x y)  then fAux (gx x) y  else ylet f y = fAux (hx x) (hy y)

• In this case, to prove anything about f, we should really be proving a property of fAux x (hy y), by induction on x.
• We need to keep x abstract since it changes over the course of recursive calls.
• We can keedp (hy y) the same, to retain information that the argument was (hy y), since it doesn't change during recursive calls.